Kerodon

Proof. Let us identify $\overline{u}$ and $\overline{u}'$ with objects $C$ and $C'$ of the slice $\infty $-category $\operatorname{\mathcal{C}}_{/u}$. Our assumption that $\overline{u}$ is a limit diagram guarantees that $C$ is a final object of $\operatorname{\mathcal{C}}_{/u}$, so there exists a morphism $f: C' \rightarrow C$ in $\operatorname{\mathcal{C}}_{/u}$. Note that $\overline{u}'$ is a limit diagram if and only if the object $C'$ is also final: that is, if and only if the morphism $f$ is an isomorphism.

Let $g: D' \rightarrow D$ be the image of $f$ under the functor $F_{/u}: \operatorname{\mathcal{C}}_{/u} \rightarrow \operatorname{\mathcal{D}}_{ / (F \circ u)}$. Our assumption that $F \circ \overline{u}$ is a limit diagram guarantees that $D$ is a final object of $\operatorname{\mathcal{D}}_{ / (F \circ u)}$. Consequently, $g$ is an isomorphism if and only if the object $D'$ is also final: that is, if and only if $(F \circ \overline{u}')$ is a limit diagram in $\operatorname{\mathcal{D}}$.

To complete the proof, it will suffice to show that $f$ is an isomorphism in $\operatorname{\mathcal{C}}_{/u}$ if and only if $g = F_{/u}(f)$ is an isomorphism in $\operatorname{\mathcal{D}}_{ / (F \circ u)}$. In fact, the functor $F_{/u}$ is conservative: this follows from our assumption that $F$ is conservative, by virtue of Corollary 4.4.2.12. $\square$