The Stacks project

Proof. The question is local around $x$, hence we may assume that $X = \mathop{\mathrm{Spec}}(A)$ for some finite type $k$-algebra. Let $x$ correspond to the prime $\mathfrak p$.

If $A$ is smooth over $k$ at $\mathfrak p$, then we may localize $A$ and assume that $A$ is smooth over $k$. In this case $k' \otimes _ k A$ is smooth over $k'$ for all extension fields $k'/k$, and each of these Noetherian rings is regular by Algebra, Lemma 10.140.3.

Assume $X$ is geometrically regular at $x$. Consider the residue field $K := \kappa (x) = \kappa (\mathfrak p)$ of $x$. It is a finitely generated extension of $k$. By Algebra, Lemma 10.45.3 there exists a finite purely inseparable extension $k'/k$ such that the compositum $k'K$ is a separable field extension of $k'$. Let $\mathfrak p' \subset A' = k' \otimes _ k A$ be a prime ideal lying over $\mathfrak p$. It is the unique prime lying over $\mathfrak p$, see Algebra, Lemma 10.46.7. Hence the residue field $K' := \kappa (\mathfrak p')$ is the compositum $k'K$. By assumption the local ring $(A')_{\mathfrak p'}$ is regular. Hence by Algebra, Lemma 10.140.5 we see that $k' \to A'$ is smooth at $\mathfrak p'$. This in turn implies that $k \to A$ is smooth at $\mathfrak p$ by Algebra, Lemma 10.137.19. The lemma is proved. $\square$