Optimal proof of a lemma

Thanks to JuanPablo
https://stacks.math.columbia.edu/tag/051F#comment-3621

algebra.tex

@@ -23245,33 +23245,15 @@ \section{Flatness criteria over Artinian rings}
 
 \begin{proof}
 The implication (2) $\Rightarrow$ (1) is immediate.
-We will prove the other implication by using induction on $n$ to show that
-$\{x_\alpha\}_{\alpha \in A}$ forms a basis for
-$M/\mathfrak m^nM$ over $R/\mathfrak m^n$. The case $n = 1$ holds by
-assumption (1). Assume the statement holds for some $n \geq 1$. By
-Nakayama's Lemma \ref{lemma-NAK}
-the elements $x_\alpha$ generate $M$, in particular $M/\mathfrak m^{n + 1}M$.
-The exact sequence
-$0 \to \mathfrak m^n/\mathfrak m^{n + 1} \to R/\mathfrak m^{n + 1} \to
-R/\mathfrak m^n \to 0$
-gives on tensoring with $M$ the exact sequence
-$$
-0 \to \mathfrak m^nM/\mathfrak m^{n + 1}M \to
-M/\mathfrak m^{n + 1}M \to
-M/\mathfrak m^nM \to 0
-$$
-Here we are using that $M$ is flat.
-Moreover, we have $\mathfrak m^nM/\mathfrak m^{n + 1}M =
-M/\mathfrak mM \otimes_{R/\mathfrak m} \mathfrak m^n/\mathfrak m^{n + 1}$
-by flatness of $M$ again.
-Now suppose that $\sum f_\alpha x_\alpha = 0$ in $M/\mathfrak m^{n + 1}M$.
-Then by induction hypothesis $f_\alpha \in \mathfrak m^n$ for each $\alpha$.
-By the short exact sequence above we then conclude that
-$\sum \overline{f}_\alpha \otimes \overline{x}_\alpha$ is zero in
-$\mathfrak m^n/\mathfrak m^{n + 1} \otimes_{R/\mathfrak m} M/\mathfrak mM$.
-Since $\overline{x}_\alpha$ forms a basis we conclude that each of the
-congruence classes $\overline{f}_\alpha \in \mathfrak m^n/\mathfrak m^{n + 1}$
-is zero and we win.
+Assume (1). By Nakayama's Lemma \ref{lemma-NAK}
+the elements $x_\alpha$ generate $M$. Then one gets a short exact
+sequence
+$$
+0 \to K \to \bigoplus\nolimits_{\alpha \in A} R \to M \to 0
+$$
+Tensoring with $R/\mathfrak m$ and using Lemma \ref{lemma-flat-tor-zero}
+we obtain $K/\mathfrak mK = 0$. By Nakayama's Lemma \ref{lemma-NAK}
+we conclude $K = 0$.
 \end{proof}
 
 \begin{lemma}