The Stacks project

Proof. Let $g : Y \to S$ and $f : X \to Y$ be local complete intersection morphisms. Let $x \in X$ and set $y = f(x)$. Choose an open neighbourhood $V \subset Y$ of $y$ and a factorization $g|_ V = \pi \circ i$ for some Koszul-regular immersion $i : V \to P$ and smooth morphism $\pi : P \to S$. Next choose an open neighbourhood $U$ of $x \in X$ and a factorization $f|_ U = \pi ' \circ i'$ for some Koszul-regular immersion $i' : U \to P'$ and smooth morphism $\pi ' : P' \to Y$. In fact, we may assume that $P' = \mathbf{A}^ n_ V$, see discussion preceding and following Definition 37.62.2. Picture:

Set $P'' = \mathbf{A}^ n_ P$. Then $U \to P' \to P''$ is a Koszul-regular immersion as a composition of Koszul-regular immersions, namely $i'$ and the flat base change of $i$ via $P'' \to P$, see Divisors, Lemma 31.21.3 and Divisors, Lemma 31.21.7. Also $P'' \to P \to S$ is smooth as a composition of smooth morphisms, see Morphisms, Lemma 29.34.4. Hence we conclude that $X \to S$ is Koszul at $x$ as desired. $\square$