Proof of Proposition 5.1.2.1.
Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of $\infty $-categories, and let $g: Y \rightarrow Z$ be a morphism in the $\infty $-category $\operatorname{\mathcal{C}}$ having image $\overline{g}: \overline{Y} \rightarrow \overline{Z}$ in the $\infty $-category $\operatorname{\mathcal{D}}$. By virtue of Proposition 5.1.1.13, the morphism $g$ is $q$-cartesian if and only if the restriction map
\[ \theta : \operatorname{\mathcal{C}}_{/g} \rightarrow \operatorname{\mathcal{C}}_{/Z} \times _{\operatorname{\mathcal{D}}_{/\overline{Z}}} \operatorname{\mathcal{D}}_{/\overline{g}} \]
is a trivial Kan fibration of simplicial sets. Since $q$ is an inner fibration, the morphism $\theta $ is a right fibration (Proposition 4.3.6.8). For each object $X \in \operatorname{\mathcal{C}}$, $\theta $ restricts to a right fibration of simplicial sets
\[ \theta _{X}: \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/g} \rightarrow \{ X\} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z} \times _{\operatorname{\mathcal{D}}_{/\overline{Z}}} \operatorname{\mathcal{D}}_{/\overline{g}}. \]
Note that if $\theta $ is a trivial Kan fibration, then so is $\theta _{X}$. Conversely, if each $\theta _{X}$ is a trivial Kan fibration, then every fiber of $\theta $ is a contractible Kan complex, so that $\theta $ is a trivial Kan fibration by virtue of Proposition 4.4.2.14. To complete the proof, it will suffice to show that $\theta _{X}$ is a trivial Kan fibration if and only if the diagram (5.3) appearing in the statement of Proposition 5.1.2.1 is a homotopy pullback square.
For the remainder of the proof, let us regard the object $X \in \operatorname{\mathcal{C}}$ as fixed, and set $\overline{X} = q(X)$. We then have a commutative diagram of simplicial sets
5.5
\begin{equation} \begin{gathered}\label{equation:mapping-space-cartesian-diagram2} \xymatrix@R =50pt@C=50pt{ \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/g} \ar [r] \ar [d] & \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z} \ar [d]^-{\rho } \\ \{ \overline{X} \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / \overline{g} } \ar [r] & \{ \overline{X} \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / \overline{Z} }. } \end{gathered} \end{equation}
Corollary 4.3.6.11 guarantees that the restriction maps
\[ \operatorname{\mathcal{C}}_{/g} \rightarrow \operatorname{\mathcal{C}}_{/Z} \rightarrow \operatorname{\mathcal{C}}\quad \quad \operatorname{\mathcal{D}}_{/\overline{g}} \rightarrow \operatorname{\mathcal{D}}_{ / \overline{Z} } \rightarrow \operatorname{\mathcal{D}} \]
are right fibrations, so that each of the simplicial sets appearing in the diagram (5.5) is a Kan complex. The morphism $\rho $ is a pullback of the restriction map $\operatorname{\mathcal{C}}_{/Z} \rightarrow \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{/ \overline{Z}}$, and is therefore a right fibration by virtue of Proposition 4.3.6.8. Applying Corollary 4.4.3.8, we deduce that $\rho $ is a Kan fibration. The projection map
\[ \{ X\} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z} \times _{\operatorname{\mathcal{D}}_{/\overline{Z}}} \operatorname{\mathcal{D}}_{/\overline{g}} \rightarrow \{ \overline{X} \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / \overline{g} } \]
is a pullback of $\rho $, and therefore also a Kan fibration. In particular, the target of the right fibration $\theta _{X}$ is a Kan complex, so that $\theta _{X}$ is a Kan fibration (Corollary 4.4.3.8). It follows that $\theta _{X}$ is a trivial Kan fibration if and only if is a homotopy equivalence (Proposition 3.3.7.6): that is, if and only if the diagram (5.5) is a homotopy pullback square.
Let $\sigma $ be an $n$-simplex of the simplicial set $\{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/g}$. Then we can identify $\sigma $ with a morphism of simplicial sets $u_{\sigma }: \Delta ^{n} \star \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$ such that $u_{\sigma }|_{\Delta ^ n}$ is the constant map taking the value $X$ and $u_{\sigma }|_{\Delta ^1} = g$. Let $\pi : \Delta ^ n \times \Delta ^2 \rightarrow \Delta ^{n} \star \Delta ^1 \simeq \Delta ^{n+2}$ be the map given on vertices by the formula
\[ \pi (i,j) = \begin{cases} i & \textnormal{ if } j = 0 \\ n+1 & \textnormal{ if } j = 1 \\ n+2 & \textnormal{ if } j = 2. \end{cases} \]
The composition $u_{\sigma } \circ \pi : \Delta ^ n \times \Delta ^2 \rightarrow \operatorname{\mathcal{C}}$ can then be regarded as an $n$-simplex $\sigma '$ of the simplicial set $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \times _{\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z)} \{ g\} $. The construction $\sigma \mapsto \sigma '$ depends functorially on $[n] \in \operatorname{{\bf \Delta }}$, and therefore determines a morphism of Kan complexes
\[ \iota ^{\mathrm{R}}_{X,g}: \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/g} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) } \{ g\} . \]
Note that the morphism $\iota _{X,g}$ fits into a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/g} \ar [d] \ar [r]^-{ \iota ^{\mathrm{R}}_{X,g} } & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \times _{\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) } \{ g\} \ar [d] \\ \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Y} \ar [r]^-{\iota ^{\mathrm{R}}_{X,Y}} & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y), } \]
where the left vertical map is a pullback of the restriction morphism $\operatorname{\mathcal{C}}_{/g} \rightarrow \operatorname{\mathcal{C}}_{/Y}$ (and therefore a trivial Kan fibration by virtue of Corollary 4.3.6.13), the right vertical map is a pullback of the restriction morphism $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z)$ (and therefore a trivial Kan fibration by virtue of Corollary 4.6.9.5), and $\iota ^{\mathrm{R}}_{X,Y}: \operatorname{Hom}^{\mathrm{R}}_{\operatorname{\mathcal{C}}}(X,Y) \hookrightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)$ is the right-pinch inclusion map of Construction 4.6.5.7 (which is a homotopy equivalence of Kan complexes by virtue of Proposition 4.6.5.10). It follows that $\iota ^{\mathrm{R}}_{X,g}$ is also a homotopy equivalence of Kan complexes. Applying the same construction to the $\infty $-category $\operatorname{\mathcal{D}}$, we obtain a homotopy equivalence
\[ \iota ^{\mathrm{R}}_{\overline{X}, \overline{g}}: \{ \overline{X} \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{/ \overline{g}} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}(\overline{X}, \overline{Y}, \overline{Z}) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{Y}, \overline{Z}) } \{ \overline{g} \} . \]
We have a commutative diagram of Kan complexes
\[ \xymatrix@R =50pt@C=10pt{ \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/g} \ar [rr] \ar [dd] \ar [dr]_{ \iota ^{\mathrm{R}}_{X,g}} & & \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z} \ar [dd] \ar [dr]_{ \iota _{X,Z}^{\mathrm{R}} } & \\ & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) } \{ g\} \ar [rr] \ar [dd] & & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z) \ar [dd] \\ \{ \overline{X} \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / \overline{g} } \ar [rr] \ar [dr]_{ \iota ^{\mathrm{R}}_{\overline{X}, \overline{g} } } & & \{ \overline{X} \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{/ \overline{Z} } \ar [dr]_{ \iota ^{\mathrm{R}}_{ \overline{X}, \overline{Z} }} & \\ & \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{X}, \overline{Y}, \overline{Z} ) \times _{ \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{Y}, \overline{Z} ) } \{ \overline{g} \} \ar [rr] & & \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{X}, \overline{Z} ), } \]
where the right-pinch inclusion maps $\iota ^{\mathrm{R}}_{X,Z}$ and $\iota ^{\mathrm{R}}_{\overline{X}, \overline{Z}}$ are homotopy equivalences (Proposition 4.6.5.10). Applying Corollary 3.4.1.12, we conclude that the front face (5.3) is a homotopy pullback square if and only if the back face (5.5) is a homotopy pullback square: that is, if and only if $\theta _{X}$ is a trivial Kan fibration.
$\square$