Proposition 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, 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, 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 It follows that $\theta : \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a left fibration (Remark, and in particular $\operatorname{\mathcal{E}}$ is an $\infty $-category (Remark

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, 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 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 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 $\square$