The Stacks project

Proof. We choose maps and objects in the following way: First write $a = s^{-1}g$ for some $s : X' \to X''$ in $S$ and $g : X \to X''$. By LMS2 we can find $t : Y' \to Y''$ in $S$ and $f'' : X'' \to Y''$ such that

commutes. Now in this diagram we are going to repeatedly change our choice of

by postcomposing both $t$ and $f''$ by a morphism $d : Y'' \to Y'''$ with the property that $d \circ t \in S$. According to Remark 4.27.7 we may after such a replacement assume that there exists a morphism $h : Y \to Y''$ such that $b = t^{-1}h$ holds¹. At this point we have everything as in the lemma except that we don't know that the left square of the diagram commutes. But the definition of composition in $S^{-1} \mathcal{C}$ shows that $b \circ Q\left(f\right)$ is the equivalence class of the pair $(h \circ f : X \to Y'', t : Y' \to Y'')$ (since $b$ is the equivalence class of the pair $(h : Y \to Y'', t : Y' \to Y'')$, while $Q\left(f\right)$ is the equivalence class of the pair $(f : X \to Y, \text{id} : Y \to Y)$), while $Q\left(f'\right) \circ a$ is the equivalence class of the pair $(f'' \circ g : X \to Y'', t : Y' \to Y'')$ (since $a$ is the equivalence class of the pair $(g : X \to X'', s : X' \to X'')$, while $Q\left(f'\right)$ is the equivalence class of the pair $(f' : X' \to Y', \text{id} : Y' \to Y')$). Since we know that $b \circ Q\left(f\right) = Q\left(f'\right) \circ a$, we thus conclude that the equivalence classes of the pairs $(h \circ f : X \to Y'', t : Y' \to Y'')$ and $(f'' \circ g : X \to Y'', t : Y' \to Y'')$ are equal. Hence using Lemma 4.27.6 we can find a morphism $d : Y'' \to Y'''$ such that $d \circ t \in S$ and $d \circ h \circ f = d \circ f'' \circ g$. Hence we make one more replacement of the kind described above and we win. $\square$