The Stacks project

Proof. It suffices to show that $\dim _{\mathfrak q}(S/k)$ is equal to $\dim (S \otimes _ R K)$ for every prime $\mathfrak q$ of $S$ containing $\mathfrak m_ RS$. Pick such a prime. By Lemma 10.125.6 the inequality $\dim _{\mathfrak q}(S/k) \geq \dim (S \otimes _ R K)$ holds. Set $n = \dim _{\mathfrak q}(S/k)$. By Lemma 10.125.2 after replacing $S$ by $S_ g$ for some $g \in S$, $g \not\in \mathfrak q$ there exists a quasi-finite ring map $R[t_1, \ldots , t_ n] \to S$. If $\dim (S \otimes _ R K) < n$, then $K[t_1, \ldots , t_ n] \to S \otimes _ R K$ has a nonzero kernel. Say $f = \sum a_ I t_1^{i_1}\ldots t_ n^{i_ n}$. After dividing $f$ by a nonzero coefficient of $f$ with minimal valuation, we may assume $f\in R[t_1, \ldots , t_ n]$ and some $a_ I$ does not map to zero in $k$. Hence the ring map $k[t_1, \ldots , t_ n] \to S \otimes _ R k$ has a nonzero kernel which implies that $\dim (S \otimes _ R k) < n$. Contradiction. $\square$