$\require{AMScd}$
Related to this, I have a question about the proof given in Kerodon of the following result:
Proposition 7.3.7.1: Let $C$ be an $\infty$-category, let $\bar{F} : C^\rhd \to D$ be a functor of $\infty$-categories, and let $U : D \to E$ be another functor of $\infty$-categories. Assume that $F = \bar{F}_{\vert C}$ is U-left Kan extended from a full subcategory $C_0 \subseteq C$. Then $\bar{F}$ is a U-colimit diagram if and only if the composite map $C_0^\rhd \to C^\rhd \to D$ is a $U$-colimit diagram.
The proof proceeds by observing that $\bar{F}$ is a $U$-colimit diagram iff for each $Y : D$, the following commutative diagram is a homotopy pullback square (regarding $D$ as a constant functor):
$$ \begin{CD} \hom(\bar{F},D) @>{}>> \hom(F,D)\\ @VVV @VVV \\ \hom(U \circ \bar{F},U(D)) @>>> \hom(U \circ F,U(D)) \end{CD} $$
Likewise, the composite is a $U$-colimit diagram if and only if for each $Y : D$ the following is a homotopy pullback square:
$$ \begin{CD} \hom(\bar{F}_{\vert C_0^\rhd},D) @>{}>> \hom(F_{\vert C_0},D)\\ @VVV @VVV \\ \hom(U \circ \bar{F}_{\vert C_0^\rhd},U(D)) @>>> \hom(U \circ F_{\vert C_0},U(D)) \end{CD} $$
Accordingly, it suffices to show that the first diagram is a pullback square if and only if the second is. Restriction maps assemble these two squares into a cube, with the first as the back face and the second as the front face. Therefore, it suffices to argue that each restriction map is a homotopy equivalence. To this end, Kerodon uses another lemma to observe that the assumption that $\bar{F}$ is $U$-Kan extended from $F$ yields two pullback squares (the left and right faces of the cube):
$$ \begin{CD} \hom(\bar{F},D) @>{}>> \hom(\bar{F}_{\vert C_0^\rhd},D)\\ @VVV @VVV \\ \hom(U \circ \bar{F},U(D)) @>>> \hom(U \circ \bar{F}_{\vert C_0^\rhd},U(D)) \end{CD} $$
$$ \begin{CD} \hom(F,D) @>{}>> \hom(F_{\vert C_0},D)\\ @VVV @VVV \\ \hom(U \circ F,U(D)) @>>> \hom(U \circ F_{\vert C_0},U(D)) \end{CD} $$
Question I fail to see how the existence of pullback squares shows that the four restriction maps are homotopy equivalences, as Kerodon indicates. It would now suffice to argue that only $\hom(U \circ F,U(D)) \to \hom(U \circ F_{\vert C_0},U(D))$ and $\hom(U \circ \bar{F},U(D)) \to \hom(U \circ \bar{F}_{\vert C_0^\rhd},U(D))$, but I cannot show this. As is, using 2-for-3 with pullbacks we can conclude that the front face being a pullback square implies that the back face is a pullback square, so the "if" is already easily shown. Is an alternative approach needed for "only if"?