SGA 1 introduces formally smooth in a very non-canonical way. The way I usually saw it introduced was through the universal lifting property, i.e., for all $A$-algebra $C$ and all $J\subset C$ nilpotent, every homomorphism $B\to C/J$ lifts to a homomorphism $B\to C$.

Grothendieck defers this definition to section 2, however, and instead spends extensive time treating the definition of formally smooth given by:

Let $u: A\to B$ be a local homomorphism of local rings, and suppose the residue field of $B$ is finite over the residue field of $A$. Then $u$ is formally smooth (or, Grothendieck states, $B$ is formally smooth over $A$) if there exists a locally finite $\hat{A}$-algebra $A'$ which is free over $\hat{A}$ such that the (and I hope I translated the French correctly here) localizations of the semi-local ring $\hat{B}\otimes_{\hat{A}}A'$ are $A'$-isomorphic to the formal series over $A'$.

I guess this definition is deferred to EGA for more intuition in the footnote, but I was wondering why this helps with our understanding of formally smooth, and how this relates to previous concepts Grothendieck introduced which would help with our understanding (e.g., does it generalize, in some sense, quasi-finite?)