Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proof. Set $p = \overline{p}|_{K}$, and let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{D}}$ denote the essential image of $F$ (Definition 4.6.2.9). Since $F \circ \overline{p}$ is a limit diagram, it is final when viewed as an object of the $\infty $-category $\operatorname{\mathcal{D}}_{ / (F \circ p)}$, hence also when viewed as an object of the full subcategory $\operatorname{\mathcal{C}}'_{ / (F \circ p)}$ (Proposition 7.1.1.20). In other words, $F \circ \overline{p}$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{C}}'$. Since the functor $F$ is fully faithful, it restricts to an equivalence of $\infty $-categories $\operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}'$ (Corollary 4.6.2.19). Applying Proposition 7.1.4.4, we conclude that $\overline{p}$ is a limit diagram in $\operatorname{\mathcal{C}}$. $\square$