Corollary 7.2.1.19. Let $f: X \rightarrow Z$ be a left cofinal morphism of simplicial sets. Then, for every simplicial set $K$, the product map $(f \times \operatorname{id}_ K): X \times K \rightarrow Z \times K$ is left cofinal.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. By virtue of Corollary 7.2.1.15, the morphism $f$ factors as a composition $X \xrightarrow {f'} Y \xrightarrow {f''} Z$, where $f'$ is left anodyne and $f''$ is a trivial Kan fibration. It follows that $f \times \operatorname{id}_{K}$ factors as a composition
\[ X \times K \xrightarrow {f' \times \operatorname{id}_ K} Y \times K \xrightarrow {f'' \times \operatorname{id}_ K } Z \times K. \]
We now note that $f' \times \operatorname{id}_{K}$ is left anodyne (Proposition 4.2.5.3) and $f'' \times \operatorname{id}_{K}$ is a trivial Kan fibration (Remark 1.5.5.2). Applying Corollary 7.2.1.15, we deduce that $f \times \operatorname{id}_{K}$ is left cofinal. $\square$