Proof.
Let $\operatorname{ev}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{E}}$ denote the evaluation morphism (given on vertices by the formula $\operatorname{ev}( F, C) = F(C)$), and let
\[ \operatorname{\mathcal{E}}' = (\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}) \star _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}} \]
denote the relative join of Construction 5.2.3.1. Note that we have a canonical map
\[ U': \operatorname{\mathcal{E}}' = (\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}) \star _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\simeq \Delta ^{1} \times \operatorname{\mathcal{C}}. \]
Let $\pi : \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ be given by projection onto the second factor. Note that $\pi $ is a cocartesian fibration, and that an edge of the product $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}$ is $\pi $-cocartesian if and only if its image in $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is an isomorphism. It follows that the $\operatorname{ev}$ carries $\pi $-cocartesian edges of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}$ to $U$-cocartesian edges of $\operatorname{\mathcal{E}}$. Applying Lemma 5.2.3.17, we deduce that $U'$ is a cocartesian fibration. By construction, we can identify $\operatorname{\mathcal{E}}$ with the inverse image of $\{ 1\} \times \operatorname{\mathcal{C}}$ under $U'$.
Let $\operatorname{\mathcal{E}}''$ denote the pushout
\[ ( \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}^{\triangleleft } ) {\coprod }_{ ( \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}^{\triangleleft } ) } \operatorname{\mathcal{E}}'. \]
Amalgamating $U'$ with the projection map $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}^{\triangleleft }$, we obtain a morphism of simplicial sets $U'': \operatorname{\mathcal{E}}'' \rightarrow K$, where $K$ denotes the pushout $( \{ 0 \} \times \operatorname{\mathcal{C}})^{\triangleleft } {\coprod }_{ ( \{ 0\} \times \operatorname{\mathcal{C}}) } ( \Delta ^1 \times \operatorname{\mathcal{C}})$. It follows from Proposition 5.1.4.7 that $U''$ is also a cocartesian fibration.
Let us abuse notation by identifying $K$ with its image in the simplicial set $( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$. Since the inclusion map $\{ 0\} \times \operatorname{\mathcal{C}}\hookrightarrow \Delta ^1 \times \operatorname{\mathcal{C}}$ is left anodyne (Proposition 4.2.5.3), the inclusion $K \hookrightarrow (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$ is inner anodyne (Example 4.3.6.5). Applying Proposition 5.6.7.2, we can write $U''$ as the pullback of a cocartesian fibration $U''': \operatorname{\mathcal{E}}''' \rightarrow (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$. We then have a commutative diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d]^{U} & \operatorname{\mathcal{E}}' \ar [r] \ar [d]^{U'} & \operatorname{\mathcal{E}}'' \ar [r] \ar [d]^{U''} & \operatorname{\mathcal{E}}''' \ar [d]^{U'''} \\ \{ 1\} \times \operatorname{\mathcal{C}}\ar [r] & \Delta ^1 \times \operatorname{\mathcal{C}}\ar [r] & K \ar [r] & ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }, } \]
where each square is a pullback and each vertical map is a cocartesian fibration. Let $\overline{\operatorname{\mathcal{E}}}$ denote the pullback $( \{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft } \times _{ (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft } } \operatorname{\mathcal{E}}'''$, so that $U'''$ restricts to a cocartesian fibration $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow ( \{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft }$. We will complete the proof by showing that the commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r] & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \\ \{ 1\} \times \operatorname{\mathcal{C}}\ar [r] & (\{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft } } \]
satisfies the requirements of Proposition 7.4.1.6.
For every simplicial subset $A \subseteq (\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$, let $\operatorname{\mathcal{D}}(A)$ denote the $\infty $-category
\[ \operatorname{Fun}_{ / A}^{\operatorname{CCart}}( A, A \times _{ ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft } } \operatorname{\mathcal{E}}'''). \]
Let ${\bf 0}$ denote the cone point of $(\Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$. Note that we have a commutative diagram of restriction functors
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}( ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft } ) \ar [r]^-{\alpha '} \ar [d]^{\beta } & \operatorname{\mathcal{D}}( (\{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft } ) \ar [d]^{\alpha } \\ \operatorname{\mathcal{D}}(K) \ar [r]^-{\beta '} \ar [d]^{\gamma } & \operatorname{\mathcal{D}}( \{ 1\} \times \operatorname{\mathcal{C}}) \\ \operatorname{\mathcal{D}}( \{ {\bf 0} \} ). & } \]
We wish to show that $\alpha $ is an equivalence of $\infty $-categories. Since the inclusion $K \hookrightarrow ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$ is inner anodyne (as noted above) and the inclusion $( \{ 1\} \times \operatorname{\mathcal{C}})^{\triangleleft } \hookrightarrow ( \Delta ^1 \times \operatorname{\mathcal{C}})^{\triangleleft }$ is left anodyne (Lemma 4.3.7.8), the morphisms $\alpha '$ and $\beta $ are trivial Kan fibrations (Proposition 5.3.1.21). It will therefore suffice to show that $\beta '$ is an equivalence of $\infty $-categories.
Amalgamating the map
\begin{eqnarray*} \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \Delta ^1 \times \operatorname{\mathcal{C}}& \simeq & (\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}) \star _{ (\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}) } (\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}) \\ & \rightarrow & (\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}) \star _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{E}}\\ & = & \operatorname{\mathcal{E}}' \end{eqnarray*}
with the identity on $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times \operatorname{\mathcal{C}}^{\triangleleft }$, we obtain a morphism of simplicial sets $F: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times K \rightarrow \operatorname{\mathcal{E}}''$. If $e$ is an edge of the product $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \times K$ whose image in $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is an isomorphism, then $F(e)$ is a $U''$-cocartesian edge of $\operatorname{\mathcal{E}}''$. We can therefore identify $F$ with a morphism of simplicial sets $f: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{D}}(K)$. Unwinding the definitions, we see that $\beta ' \circ f$ is an isomorphism of simplicial sets. Consequently, to show that $\beta '$ is an equivalence of $\infty $-categories, it will suffice to show that $f$ is an equivalence of $\infty $-categories. Similarly, the composite map $\gamma \circ f$ is an isomorphism, so we are reduced to proving that $\gamma $ is an equivalence of $\infty $-categories. Since $\beta $ is a trivial Kan fibration, this is equivalent to the assertion that $\gamma \circ \beta $ is an equivalence of $\infty $-categories, which is a special case of Corollary 5.3.1.23.
$\square$