Proof of Proposition 5.2.4.5.
The diagram (5.24) determines a morphism of simplicial sets
\[ \lambda _ X: (\Delta ^1 \times X) {\coprod }_{ ( \{ 1\} \times X) } Y \rightarrow X \star _{Y} Y, \]
and we wish to show that $\lambda _{X}$ is a categorical equivalence of simplicial sets (obtained by applying Construction 5.3.4.7 to the diagram $[1] \rightarrow \operatorname{Set_{\Delta }}$ determined by the morphism $f$). We wish to show that $\lambda _{X}$ is a categorical equivalence of simplicial sets (Proposition 4.5.4.11). By virtue of Corollary 4.5.7.3, it will suffice to prove that for every map $\Delta ^{n} \rightarrow Y$, the induced map
\[ \Delta ^{n} \times _{Y} ((\Delta ^1 \times X) {\coprod }_{ ( \{ 1\} \times X ) } Y) \rightarrow \Delta ^{n} \times _{Y} ( X \star _{Y} Y ) \]
is a categorical equivalence. Using Remark 5.2.3.9, we can replace $Y$ by $\Delta ^ n$ and $X$ by the fiber product $\Delta ^ n \times _{Y} X$, and thereby reduce the proof of Proposition 5.2.4.5 to the special case where $Y = \Delta ^ n$ is a standard simplex.
Since the collection of categorical equivalences is closed under the formation of filtered colimits (Corollary 4.5.7.2), we may assume without loss of generality that the simplicial set $X$ is finite (see Remark 3.6.1.8). In particular, $X$ has dimension $\leq m$ for some integer $m \geq -1$. We proceed by induction on $m$. If $m = -1$, then $X$ is empty and the morphism $\lambda _{X}$ is an isomorphism (see Example 5.2.3.4). Assume that $m \geq 0$; we now proceed by induction on the number of nondegenerate $m$-simplices of $X$. If $X$ does not have dimension $\leq m-1$, then a choice of nondegenerate $m$-simplex of $X$ determines a pushout diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ m \ar [r] \ar [d] & \Delta ^ m \ar [d] \\ X' \ar [r] & X, } \]
where the horizontal maps are monomorphisms (Proposition 1.1.4.12). We then obtain a cubical diagram
\[ \xymatrix@R =50pt@C=10pt{ (\Delta ^1 \times \operatorname{\partial \Delta }^ m) {\coprod }_{ ( \{ 1\} \times \operatorname{\partial \Delta }^ m ) } Y \ar [dr]_{ \lambda _{ \operatorname{\partial \Delta }^{m} }} \ar [rr] \ar [dd] & & (\Delta ^1 \times \Delta ^ m) {\coprod }_{ ( \{ 1\} \times \Delta ^ m ) } Y \ar [dr]_{ \lambda _{\Delta ^{m}} } \ar [dd] & \\ & \operatorname{\partial \Delta }^ m \star _{Y} Y \ar [dd] \ar [rr] & & \Delta ^{m} \star _{Y} Y \ar [dd] \\ (\Delta ^1 \times X' ) {\coprod }_{ (\{ 1\} \times X')} Y \ar [dr]_{\lambda _{X'} } \ar [rr] & & (\Delta ^1 \times X) {\coprod }_{ (\{ 1\} \times X)} Y \ar [dr]_{\lambda _{X} } & \\ & X' \star _{Y} Y \ar [rr] & & X \star _{Y} Y, } \]
where the front and back faces are categorical pushout squares (Proposition 4.5.4.11). Our inductive hypothesis guarantees that the morphisms $\lambda _{X'}$ and $\lambda _{\operatorname{\partial \Delta }^ m}$ are categorical equivalences. Consequently, to show that $\lambda _{X}$ is a categorical equivalence, it will suffice to show that $\lambda _{\Delta ^ m}$ is a categorical equivalence. We can therefore replace $X$ by $\Delta ^ m$, and thereby reduce the proof of Proposition 5.2.4.5 to the special case where $f: \Delta ^{m} \rightarrow \Delta ^{n}$ is a morphism between standard simplices.
Suppose that $f(m) < n$. In this case, we can identify $f$ with a morphism from $X = \Delta ^{m}$ to the simplex $\Delta ^{n-1}$ (regarded as a simplicial subset of $\Delta ^{n}$), and we can identify $X \star _{Y} Y$ with the right cone $( X \star _{\Delta ^{n-1} } \Delta ^{n-1} )^{\triangleright }$. Under this identification, $\lambda _{X}$ corresponds to the composition
\begin{eqnarray*} (\Delta ^1 \times X) {\coprod }_{ (\{ 1\} \times X)} (\Delta ^{n-1})^{\triangleright } & \xrightarrow {\lambda '} & (\Delta ^1 \times X)^{\triangleright } {\coprod }_{ (\{ 1\} \times X)^{\triangleright }} (\Delta ^{n-1})^{\triangleright } \\ & \simeq & (\Delta ^1 \times X) {\coprod }_{ (\{ 1\} \times X)} (\Delta ^{n-1} )^{\triangleright } \\ & \xrightarrow {\lambda ''} & ( X \star _{\Delta ^{n-1} } \Delta ^{n-1} )^{\triangleright }, \end{eqnarray*}
where $\lambda '$ is a pushout of the map
\[ ( \Delta ^1 \times X) {\coprod }_{ ( \{ 1\} \times X )} ( \{ 1\} \times X)^{\triangleright } \rightarrow (\Delta ^1 \times X)^{\triangleright } \]
and is therefore inner anodyne by virtue of Example 4.3.6.5 (since the inclusion $\{ 1\} \times X \hookrightarrow \Delta ^1 \times X$ is right anodyne; see Proposition 4.2.5.3). Consequently, to show that $\lambda _{X}$ is a categorical equivalence, it will suffice to show that $\lambda ''$ is a categorical equivalence. By virtue of Corollary 4.5.8.9, we are reduced to proving Proposition 5.2.4.5 for the map $f: X \rightarrow \Delta ^{n-1}$. Applying this argument repeatedly, we can reduce to the case where $f(m) = n$.
Let $Z(0)$ denote the simplicial subset of $\Delta ^1 \times \Delta ^ m$ given by the union of $\Delta ^1 \times \operatorname{\partial \Delta }^ m$ with $\{ 1\} \times \Delta ^ m$, and let
\[ Z(0) \subset Z(1) \subset Z(2) \subset \cdots \subset Z(m) \subset Z(m+1) = \Delta ^1 \times \Delta ^ m \]
be the sequence of simplicial subsets appearing in Lemma 3.1.2.12. Note that $\lambda _{X}$ carries $Z(m)$ into the simplicial subset $\operatorname{\partial \Delta }^ m \star _{Y} Y \subseteq X \star _{Y} Y$. We therefore obtain a cubical diagram of simplicial sets
\[ \xymatrix@R =50pt@C=40pt{ Z(0) \ar [dr] \ar [rr] \ar [dd] & & (\Delta ^1 \times \operatorname{\partial \Delta }^ m) {\coprod }_{ (\{ 1\} \times \operatorname{\partial \Delta }^ m) } Y \ar [dr]_{ \lambda _{\operatorname{\partial \Delta }^ m} } \ar [dd] & \\ & Z(m) \ar [rr] \ar [dd] & & \operatorname{\partial \Delta }^{m} \star _{Y} Y \ar [dd] \\ \Delta ^{1} \times \Delta ^{m} \ar [dr]_{\operatorname{id}} \ar [rr] & & (\Delta ^{1} \times \Delta ^ m) {\coprod }_{ (\{ 1\} \times \Delta ^ m) } Y \ar [dr]_{ \lambda _{\Delta ^{m}} } & \\ & \Delta ^{1} \times \Delta ^{m} \ar [rr] & & \Delta ^{m} \star _{Y} Y } \]
where the front and back faces are pushout squares and the vertical maps are monomorphisms. It follows that the front and back faces are categorical pushout squares (Example 4.5.4.12). Our inductive hypothesis guarantees that $\lambda _{\operatorname{\partial \Delta }^{m}}$ is a categorical equivalence, and the inclusion $Z(0) \hookrightarrow Z(m)$ is inner anodyne by construction (see Lemma 3.1.2.12). Applying Proposition 4.5.4.9, we conclude that $\lambda _{\Delta ^ m}$ is also a categorical equivalence.
$\square$