From this answer I learned that Grothendieck proved the following result.

**Theorem.** Every formally smooth morphism between locally noetherian schemes is flat.

The book *Smoothness, Regularity, and Complete Intersection* by Majadas and Rodicio cites the following result.

**Theorem.** Let $(A,\mathfrak m,K)\to (B,\mathfrak n, L)$ be a local homomorphism of noetherian local rings. Then TFAE.

- $B$ is a formally smooth $A$ algebra for the $\mathfrak n$-adic topology;
- $B$ is a flat $A$-module and the $K$ algebra $B\otimes_AK$ is geometrically regular.

The authors then write:

This result is due to Grothendieck [EGA 0$_{\rm{IV}}$ , (19.7.1)]. His proof is long, though it provides a lot of additional information. He uses this result in proving Cohen’s theorems on the structure of complete noetherian local rings. An alternative proof of (I) was given by M. André [An1], based on André –Quillen homology theory; it thus uses simplicial methods, that are not necessarily familiar to all commutative algebraists. A third proof was given by N. Radu [Ra2], making use of Cohen’s theorems on complete noetherian local rings.

**Questions:**

- Are there any English references for the proof of Grothendieck or of André?
- What is the
*conceptual*outline of Grothendieck's proof?

André's *Homologie des Algèbres Commutatives* does not look very geometric to a novice like me and I was hoping perhaps Grothendieck's path was more geometric. I would also like to at least glimpse the big picture of the proof.