The Stacks project

Proof. In great generality there is a pullback map $g^{-1}f_*\mathcal{F} \to f'_*(g')^{-1}\mathcal{F}$, see Sites, Section 7.45. We claim that this map sends $g^{-1}f_!\mathcal{F}$ into the subsheaf $f'_!(g')^{-1}\mathcal{F}$ and induces the isomorphism in the lemma.

Choose a geometric point $\overline{y}': \mathop{\mathrm{Spec}}(k) \to Y'$ and denote $\overline{y} = g \circ \overline{y}'$ the image in $Y$. There is a commutative diagram

where the horizontal maps were used in the proof of Lemma 63.3.11 and the vertical maps are the pullback maps above. The diagram commutes because each of the four maps in question is given by pulling back local sections along a morphism of schemes and the underlying diagram of morphisms of schemes commutes. Since the diagram in the statement of the lemma is cartesian we have $X'_{\overline{y}'} = X_{\overline{y}}$. Hence by Lemma 63.3.11 and its proof we obtain a commutative diagram

where the horizontal arrows of the inner square are isomorphisms and the two right vertical arrows are equalities. Also, the se, sw, ne, nw arrows are injective. It follows that there is a unique bijective dotted arrow fitting into the diagram. We conclude that $g^{-1}f_!\mathcal{F} \subset g^{-1}f_*\mathcal{F} \to f'_*(g')^{-1}\mathcal{F}$ is mapped into the subsheaf $f'_!(g')^{-1}\mathcal{F} \subset f'_*(g')^{-1}\mathcal{F}$ because this is true on stalks, see Étale Cohomology, Theorem 59.29.10. The same theorem then implies that the induced map is an isomorphism and the proof is complete. $\square$