$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 11.5.0.80. Suppose we are given a commutative diagram of $\infty $-categories
\[ \xymatrix { \operatorname{\mathcal{C}}' \ar [r]^-{F'} \ar [d] & \operatorname{\mathcal{D}}' \ar [r] \ar [d] & \operatorname{\mathcal{E}}' \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{F} & \operatorname{\mathcal{D}}\ar [r]^-{G} & \operatorname{\mathcal{E}}} \]
where both squares are pullbacks. Assume that $G$ and $G \circ F$ are isofibrations. If $F$ is an equivalence of $\infty $-categories, then $F'$ is an equivalence of $\infty $-categories.
Proof.
We will verify that $F'$ satisfies the criterion of Theorem 4.5.7.1. Let $X$ be a simplicial set, and consider the commutative diagram of Kan complexes
\[ \xymatrix { \operatorname{Fun}(X,\operatorname{\mathcal{C}}')^{\simeq } \ar [r]^-{F'_ X} \ar [d] & \operatorname{Fun}(X,\operatorname{\mathcal{D}}')^{\simeq } \ar [r] \ar [d] & \operatorname{Fun}(X,\operatorname{\mathcal{E}}')^{\simeq } \ar [d] \\ \operatorname{Fun}(X,\operatorname{\mathcal{C}})^{\simeq } \ar [r]^-{F_ X} & \operatorname{Fun}(X,\operatorname{\mathcal{D}})^{\simeq } \ar [r]^-{G_ X} & \operatorname{Fun}(X,\operatorname{\mathcal{E}})^{\simeq }. } \]
We wish to show that the morphism $F'_{X}$ is a homotopy equivalence. Using Corollaries 4.4.5.6 and 4.4.3.19, we see that the right square and outer rectangle are homotopy pullback diagrams. It follows that the left square is also a homotopy pullback diagram (Proposition 3.4.1.11). Since $F$ is an equivalence of $\infty $-categories, the morphism $F_{X}$ is a homotopy equivalence of Kan complexes (Theorem 4.5.7.1). Applying Corollary 3.4.1.5, we deduce that $F'_{X}$ is also a homotopy equivalence of Kan complexes.
$\square$