Kerodon

Proof. Let $\widetilde{u}: X' \times _{S} S_{ (q \circ f) / } \rightarrow X \times _{S} S_{ (q \circ f) /}$ denote the pullback of $u$, let $\widetilde{q}: X \times _{S} S_{ (q \circ f) /} \rightarrow S_{ (q \circ f) / }$ be given by projection onto the second factor, and let $v: X_{ f/} \rightarrow X \times _{S} S_{ (q \circ f)/ }$ be the left fibration of Proposition 4.3.6.8. Note that $\widetilde{q}$ is a pullback of $q$, and therefore a cartesian fibration (Remark 5.1.4.6). Moreover, an edge of $X \times _{S} S_{ (q \circ f) /}$ is $\widetilde{q}$-cartesian if and only if its image in $X$ is $q$-cartesian. Similarly, the composite map $\widetilde{q} \circ \widetilde{u}$ is a pullback of $q'$. It follows that $\widetilde{q} \circ \widetilde{u}$ is a cartesian fibration, and that an edge of $X' \times _{S} S_{ (q \circ f) / }$ is $(\widetilde{q} \circ \widetilde{u})$-cartesian if and only if its image in $X'$ is $q'$-cartesian. Applying Proposition 5.1.4.19, we deduce that the composition $\widetilde{q} \circ v$ is a cartesian fibration, and that an edge of $X_{ f/}$ is $(\widetilde{q} \circ v)$-cartesian if and only if its image in $X$ is $q$-cartesian. The desired result now follows by applying Proposition 5.1.4.20 to the diagram