The Stacks project

Proof. Choose a diagram

as in Lemma 15.39.3. Let $t_1, \ldots , t_ d$ be a regular system of parameters for $R$ with $t_1 = p$ in case the characteristic of $k$ is $p > 0$. As $B$ and $\overline{S} = S \otimes _ R k$ are regular we see that $\mathop{\mathrm{Ker}}(\overline{S} \to B)$ is generated by elements $\overline{x}_1, \ldots , \overline{x}_ r$ which form part of a regular system of parameters of $\overline{S}$, see Algebra, Lemma 10.106.4. Lift these elements to $x_1, \ldots , x_ r \in S$. Then $t_1, \ldots , t_ d, x_1, \ldots , x_ r$ is part of a regular system of parameters for $S$. Hence $S/(x_1, \ldots , x_ r)$ is a power series ring over a field (if the characteristic of $k$ is zero) or a power series ring over a Cohen ring (if the characteristic of $k$ is $p > 0$), see Lemma 15.39.2. Moreover, it is still the case that $R \to S/(x_1, \ldots , x_ r)$ maps $t_1, \ldots , t_ d$ to a part of a regular system of parameters of $S/(x_1, \ldots , x_ r)$. In other words, we may replace $S$ by $S/(x_1, \ldots , x_ r)$ and assume we have a diagram

as in Lemma 15.39.3 with moreover $\overline{S} = B$. In this case $R \to S$ is formally smooth in the $\mathfrak m_ S$-adic topology by Proposition 15.40.5. Hence the base change $C = S \otimes _ R A$ is formally smooth over $A$ in the $\mathfrak m_ C$-adic topology by Lemma 15.37.8. $\square$