Kerodon

Corollary 7.3.7.4. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be a functor of $\infty $-categories, and let $V': \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ be the functor given by postcomposition with $V'$. Suppose we are given another functor $f: \operatorname{\mathcal{A}}\rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ and a full subcategory $\operatorname{\mathcal{A}}^{0} \subseteq \operatorname{\mathcal{A}}$. If the induced map $\operatorname{\mathcal{A}}\times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is $V$-left Kan extended from $\operatorname{\mathcal{A}}^{0} \times \operatorname{\mathcal{C}}$, then $f$ is $V'$-left Kan extended from $\operatorname{\mathcal{A}}^{0}$.