Morphism whose fibers are finite and reduced is unramified

Definition: Let $f: X \to Y$ be a morphism of finite type of locally Noetherian schemes, $x \in X, y = f(x) \in Y$. Say that $f$ is unramified at $x$ if the map on stalks satisfies $m_y \mathcal{O}_{X,x} = m_x$ and the extension $k(y) \to k(x)$ is separable.

Proposition: If $f$ is as above, and for every $y \in Y$, the fibers $X_y$ are finite, reduced, and $k(x)/k(y)$ is separable, then $f$ is unramified.

I observe that the quotient $\mathcal{O}_{X,x} / m_y \mathcal{O}_{X,x}$ is the same when replacing $X$ with fiber $X_y$. Evidently this implies the above proposition.

Taking the observation, it seems we want to show that $\mathcal{O}_{X_y,x} / m_y \mathcal{O}_{X_y,x} = k(x)$, the residue field at $x$.

Since $X_y$ is finite (although it doesn't specify, I'm assuming it means over $\text{Spec } k(y)$), then I know that it is a finite dimensional vector space over $k(y)$. Reduced tells me that there are no nilpotent elements in $\mathcal{O}_{X_y,x}$.

Since the question is stalk-wise, I'm not sure how to apply finite. Should I take an open affine neighborhood of $y$ and then pull back to an open affine neighborhood cut out by a finite module? But this doesn't seem to help in showing that the maximal ideal in the local ring coincide.

My current idea is to look at the map $X_y \to X$. The map on stalks is then given by $\mathcal{O}_{X,x} \to \mathcal{O}_{X,x} \otimes k(y) = \mathcal{O}_{X_y,x}$ and try to show that this map has kernel $m_x$. Furthermore, this is a local homomorphism so the contraction of the maximal ideal in the fiber is $m_x$.

My problem is that I'm not seeing where any of the assumptions will come into play or how to proceed further.

I will turn my comments into an answer. The condition "finite" here means that $X_y$ contains finitely many points. In other words, $X_y$ is of dimension zero. In particular, $X_y$ is affine, so $X_y=\operatorname{Spec}(R)$ and since $R$ is Noetherian of dimension zero, it is Artinian. Hence, $\mathcal O_{X_y,x}$ is local, reduced and Artinian, therefore a field. This implies $\mathfrak m_y \mathcal O_{X_y,x} = (0)$ because $1\notin\mathfrak m_y$, so you have $k(x)=\mathcal O_{X_y,x}/\mathfrak m_y \mathcal O_{X_y,x}$ as desired.

$X_y$ is finite means it has finite points.

Step 1: Show $X_y$ is a Noetherian scheme.

Hint: finite type morphism is stable under base change, and Lemma 28.14.6 Stack Project.

Step 2: Show $X_y$ is an algebraic variety over $k(y)$. (Using Liu's notation).

Trivial.

Step 3: Show $X_y$ is discrete.

Hint: The set of closed points in an algebraic variety is dense. (Remark 2.3.49 in Liu's book).

Step 4: Take a point $x\in X_y$ and an open affine neighborhood $\mathrm {Spec} \ R,$ denote $p$ the prime ideal represented by $x$. Show $R$ has Krull dimension $0$.

Hint: Given a Noetherian ring A, it has krull dimension 0 if and only if $\mathrm{Spec} A$ is discrete and finite. from this wiki page.

Step 5: Show $R_p$ is a local reduced Noetherian ring with Krull dimension $0$.

Trivial.

Step 6: Show $R_p=\mathcal O_{{X_y},x}=\mathcal O_{X,x}/\mathfrak m_y\mathcal O_{X,x}$ is a field.

Local + dimension $0$ imply the maximal ideal is the only prime ideal, hence the nilradical, which is zero by reducedness. Thus the ring is a field.

Step 7: Show $\mathfrak m_y\mathcal O_{X,x}=\mathfrak m_x$.

Trivial.