Let $k$ be a field, $R:=k[x_1, \cdots , x_n]$ and $\mathfrak m$ be a maximal ideal such that $R/\mathfrak m$ is a finite separable field extension of $k$. Consider the algebraic closure $\overline k$ of $k$ and let $\mathfrak m_1, \dots , \mathfrak m_r$ be the maximal ideals of the ring $$\overline R :=\overline k \otimes_k R = \overline k[x_1, \cdots , x_n]$$ lying over $\mathfrak m$.
In an article I have been reading, the following isomorphism is used $$\overline k \otimes_k R/\mathfrak m \cong \overline R \big/ \bigcap_{1 \leq j \leq r} \mathfrak m_j$$ and the only justification given for it is that since the extension $R/\mathfrak m$ over $k$ is separable, $\overline k \otimes_k R/\mathfrak m$ is a reduced ring.
Now with some help from a Math Overflow user, I have been able to justify this isomorphism here (https://mathoverflow.net/questions/391773/base-change-to-algebraic-closure-commutes-with-quotient-of-polynomial-ring-by-ma), but it I am not sure where I am needing this separability assumption anywhere in the justification.
Moreover, this isomorphism is part of a bigger proposition, one of the hypotheses of which is the aforementioned separability of extensions, and it seems like this isomorphism is the only place where the above hypothesis gets used. Upon further enquiry about the same (in the comment section of the linked post), I was advised to ask this here, hence my question is the following:
Is the justification in the linked post correct? If so, where do I need the separability of extensions, more precisely the reducedness of the ring $\overline k \otimes_k R/\mathfrak m$ that seems to come as a consequence of the same? If not, I would really appreciate a correct justification or reference (most probably using the reducedness hypothesis) for the above isomorphism. Thank you.