Proposition 4.4.2.13. Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of $\infty $-categories, let $u$ be an isomorphism in $\operatorname{\mathcal{C}}$, let $n \geq 2$ be an integer, and suppose we are given a lifting problem
\[ \xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{n} \ar [r]^-{ \sigma _0} \ar [d] & \operatorname{\mathcal{C}}\ar [d]^{q} \\ \Delta ^{n} \ar@ {-->}[ur]^{\sigma } \ar [r]^-{ \overline{\sigma } } & \operatorname{\mathcal{D}}. } \]
If the composite map
\[ \Delta ^{1} \simeq \operatorname{N}_{\bullet }( \{ n-1 < n \} ) \hookrightarrow \Lambda ^{n}_ n \xrightarrow {\sigma _0} \operatorname{\mathcal{C}} \]
is equal to $u$, then there exists an $n$-simplex $\sigma : \Delta ^{n} \rightarrow \operatorname{\mathcal{C}}$ rendering the diagram commutative.
Proof.
Using Lemma 4.3.6.16, we can identify the horn $\Lambda ^{n}_{n}$ with the pushout
\[ (\Delta ^{n-2} \star \{ 1\} ) \coprod _{ ( \operatorname{\partial \Delta }^{n-2} \star \{ 1\} ) } ( \operatorname{\partial \Delta }^{n-2} \star \Delta ^1) \subseteq \Delta ^{n-2} \star \Delta ^1 \simeq \Delta ^{n}. \]
Set $f= \sigma _0|_{ \Delta ^{n-2} }$ and $f_0 = \sigma _0|_{ \operatorname{\partial \Delta }^{n-2} }$, and let $\operatorname{\mathcal{E}}$ denote the fiber product $\operatorname{\mathcal{C}}_{f_0/} \times _{\operatorname{\mathcal{D}}_{ (q \circ f_0)/}} \operatorname{\mathcal{D}}_{( q \circ f)/}$. Note that there is an evident projection map $\theta : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, given by the composition
\[ \operatorname{\mathcal{E}}\xrightarrow {\theta '} \operatorname{\mathcal{C}}_{f_0/} \xrightarrow {\theta ''} \operatorname{\mathcal{C}}. \]
The morphism $\theta ''$ is a left fibration (Proposition 4.3.6.1), and the morphism $\theta '$ is a pullback of the restriction map $\operatorname{\mathcal{D}}_{(q \circ f)/} \rightarrow \operatorname{\mathcal{D}}_{(q \circ f_0)/}$ and is therefore also a left fibration (Corollary 4.3.6.14). It follows that $\theta : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Remark 4.2.1.11), and in particular $\operatorname{\mathcal{E}}$ is an $\infty $-category (Remark 4.1.1.9).
Note that the restriction of $\sigma _0$ to $\Delta ^{n-2} \star \{ 1\} $ can be identified with an object $Y$ of the coslice $\infty $-category $\operatorname{\mathcal{C}}_{f/}$. Let
\[ \rho : \operatorname{\mathcal{C}}_{f/} \rightarrow \operatorname{\mathcal{C}}_{f_0/} \times _{ \operatorname{\mathcal{D}}_{ ( q \circ f_0)/ }} \operatorname{\mathcal{D}}_{(q \circ f)/} = \operatorname{\mathcal{E}} \]
be the left fibration of Proposition 4.3.6.8, and set $\overline{Y} = \rho (Y) \in \operatorname{\mathcal{E}}$. Then the restriction $\sigma _0|_{ \operatorname{\partial \Delta }^{n-2} \star \Delta ^1}$ and $\overline{\sigma }$ determine a morphism $\overline{v}: \overline{X} \rightarrow \overline{Y}$ in the $\infty $-category $\operatorname{\mathcal{E}}$. Unwinding the definitions, we see that choosing an $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ satisfying the requirements of Proposition 4.4.2.13 is equivalent to choosing a morphism $v: X \rightarrow Y$ in $\operatorname{\mathcal{C}}_{f/}$ satisfying $\rho (v) = \overline{v}$. Since $\rho $ is a left fibration, it is an isofibration (Example 4.4.1.11). Consequently, to prove the existence of $v$, it will suffice to show that $\overline{v}$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}$. Since $\theta $ is a left fibration, this follows from our assumption that $u = \theta ( \overline{v} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$ (Proposition 4.4.2.11).
$\square$