Proposition 9.4.6.24. Let $\operatorname{\mathcal{C}}$ be a simplicial set, let $\operatorname{\mathcal{C}}_0 \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset which contains every vertex of $\operatorname{\mathcal{C}}$, and let $U_0: \operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{C}}_0$ be a flat inner fibration. If the inclusion map $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is inner anodyne, then there exists a pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_0 \ar [d]^{U_0} \ar [r] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \operatorname{\mathcal{C}}_0 \ar [r] & \operatorname{\mathcal{C}}, } \]
where $U$ is a flat inner fibration.
Proof.
Choose an uncountable regular cardinal $\kappa $ for which the inner fibration $U_0$ is essentially $\kappa $-small. Using Theorem 9.4.4.1, we can choose a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}_0 \ar [rr]^-{H_0} \ar [dr]_{U_0} & & \widehat{\operatorname{\mathcal{E}}}_0 \ar [dl]^{ \widehat{U}_0 } \\ & \operatorname{\mathcal{C}}& } \]
which exhibits $\widehat{\operatorname{\mathcal{E}}}_0$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}_0$. Let $\operatorname{\mathcal{E}}'_0$ be the full simplicial subset of $\widehat{\operatorname{\mathcal{E}}}_0$ spanned by those vertices which belong to the image of $H_0$. It follows from Remark 9.4.1.15 that $H_0$ induces an equivalence $\operatorname{\mathcal{E}}_0 \rightarrow \operatorname{\mathcal{E}}'_0$ of inner fibrations over $\operatorname{\mathcal{C}}_0$. Using Lemma 5.6.7.1 (and Remark 9.4.6.3), we can replace $\operatorname{\mathcal{E}}_0$ by $\operatorname{\mathcal{E}}'_0$ and thereby reduce to the case where $H_0$ is an isomorphism from $\operatorname{\mathcal{E}}_0$ onto a full simplicial subset of $\widehat{\operatorname{\mathcal{E}}}_0$.
Since $U_0$ is flat, the morphism $\widehat{U}_0$ is a cartesian fibration (Proposition 9.4.6.9). Using Proposition 5.6.7.2, we can choose a pullback diagram
\[ \xymatrix@R =50pt@C=50pt{ \widehat{\operatorname{\mathcal{E}}}_0 \ar [r] \ar [d]^{ \widehat{U}_0 } & \widehat{\operatorname{\mathcal{E}}} \ar [d]^{ \widehat{U} } \\ \operatorname{\mathcal{C}}_0 \ar [r]^-{ \iota } & \operatorname{\mathcal{C}}} \]
where $\widehat{U}$ is a cartesian fibration. Let $\operatorname{Tr}_{\widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \rightarrow \mathrm{h} \mathit{\operatorname{\mathcal{QC}}}$ be the homotopy transport representation of $\widehat{U}$. Since $\iota $ induces an isomorphism of homotopy categories $\mathrm{h} \mathit{ \operatorname{\mathcal{C}}_0 } \xrightarrow {\sim } \mathrm{h} \mathit{\operatorname{\mathcal{C}}}$, Proposition 9.4.1.16 guarantees that the functor $\operatorname{Tr}_{\widehat{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}}$ carries each object of $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ to a $\kappa $-cocomplete $\infty $-category and each morphism of $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ to a functor which preserves $\kappa $-small colimits.
Let $\operatorname{\mathcal{E}}\subseteq \widehat{\operatorname{\mathcal{E}}}$ be the full simplicial subset spanned by those vertices which belong to the image of $\operatorname{\mathcal{E}}_0$, and set $U = \widehat{U}|_{\operatorname{\mathcal{E}}}$. Applying the criterion of Proposition 9.4.1.16, we see that the diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [rr] \ar [dr]_{U} & & \widehat{\operatorname{\mathcal{E}}} \ar [dl]^{ \widehat{U} } \\ & \operatorname{\mathcal{C}}& } \]
exhibits $\widehat{\operatorname{\mathcal{E}}}$ as a fiberwise $\kappa $-cocompletion of $\operatorname{\mathcal{E}}$. Since $\widehat{U}$ is a cartesian fibration, Proposition 9.4.6.9 guarantees that the inner fibration $U$ is flat. By construction, the isomorphism $\widehat{\operatorname{\mathcal{E}}}_0 \xrightarrow {\sim } \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \widehat{\operatorname{\mathcal{E}}}$ restricts to an isomorphism of $\operatorname{\mathcal{E}}_0$ with the fiber product $\operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$.
$\square$