Smooth morphisms are exactly the formally smooth locally finitely presented morphisms

Reduction to affine rings. Both smoothness at a point, local finite presentation and formal smoothness are conditions on the germ of $f$; fix $x\in X$ with $s=f(x)$, choose affine opens $U=\mathrm{Spec}C\subseteq X$ of $x$ and $V=\mathrm{Spec}A\subseteq S$ of $s$ with $f(U)\subseteq V$ and let $\mathfrak{q}\subseteq C$ be the prime of $x$. Since $f$ is locally of finite presentation, $A\to C$ is a ring map of finite presentation; write $C=P\mathrm{/}I$ with $P=A[t_1,\dots ,t_m]$ and $I=(h_1,\dots ,h_s)$ finitely generated.

Smooth implies formally smooth, at the level of standard smooth charts. Assume $f$ smooth at $x$. By [F4] the finitely presented map $A\to C$ is standard smooth at $\mathfrak{q}$: after inverting $b\in C\setminus \mathfrak{q}$, there are $m\ge r\ge 0$, polynomials $f_1,\dots ,f_r$ in $A[t_1,\dots ,t_m]$ and $g$ with $C_b\cong (A[t_1,\dots ,t_m]\mathrm{/}(f_1,\dots ,f_r){)}_g$, and some $r\times r$ Jacobian minor becomes a unit. Consider an arbitrary affine square-zero lifting problem $D^{\mathrm{\prime }}\twoheadrightarrow D$ of $A$-algebras, with kernel $J$, together with an $A$-algebra map $u:C_b\to D$. Choose lifts $T_i\in D^{\mathrm{\prime }}$ of $u(t_i)\in D$; the polynomial ring is free, so these choices define an $A$-algebra map from $A[t_1,\dots ,t_m]$ to $D^{\mathrm{\prime }}$. Its values $f_j(T)$ lie in $J$. For ${\delta }_i\in J$, the square-zero Taylor identity is $f_j(T+\delta )=f_j(T)+{\sum }_i(\mathrm{\partial }{f}_j\mathrm{/}\mathrm{\partial }{t}_i)(T){\delta }_i$. The chosen Jacobian minor maps to a unit of $D$, hence lifts to a unit of $D^{\mathrm{\prime }}$: if a lift $v$ of its inverse satisfies $uv=1+j$ with $j\in J$, then $(1+j{)}^{-1}=1-j$. Solve the resulting $r\times r$ linear system with the other ${\delta }_i=0$ to kill all $f_j$. The corrected map sends $g$ to a unit because its image in $D$ is $u(g)$, a unit, so it extends to $C_b\to D^{\mathrm{\prime }}$. Affine neighbourhoods in a general test thickening reduce its lifting diagram to this ring problem around each point; standard smooth charts cover $X$ when $f$ is smooth. This proves formal smoothness.

Formally smooth and locally of finite presentation imply smooth. Assume now that $f$ is locally of finite presentation and formally smooth. In the affine chart of step 1.1, apply formal smoothness [F3] to the square-zero thickening $\mathrm{Spec}(P\mathrm{/}{I}^2)\to \mathrm{Spec}(P\mathrm{/}I)=\mathrm{Spec}C$ and the identity of $\mathrm{Spec}C$: since $(I\mathrm{/}{I}^2{)}^2=0$ in $P\mathrm{/}{I}^2$, locally on $\mathrm{Spec}(P\mathrm{/}{I}^2)$ there is a lift, that is to say, after inverting some $b\mathrm{\notin }\mathfrak{q}$ there is an $A$-algebra section $\sigma \text{\hspace{0.17em}⁣}:C_b\to (P\mathrm{/}{I}^2{)}_b$ of the projection, so that the composite $C_b\to (P\mathrm{/}{I}^2{)}_b\to C_b$ is the identity.

Conormal splitting. Write $\sigma ({\bar{t}}_i)=t_i-g_i$ in $(P\mathrm{/}{I}^2{)}_b$ with $g_i\in I_b$, where ${\bar{t}}_i$ is the image of $t_i$; this is possible because $\sigma$ is a section. For every $f\in I_b$ the element $f(\sigma (\bar{t}))=\sigma (\bar{f})$ is zero, and the Taylor expansion at $t$ with increments $-g$ gives $f(t-g)\equiv f(t)-{\sum }_i(\mathrm{\partial }f\mathrm{/}\mathrm{\partial }{t}_i)(t)g_i$ modulo $I_b^2$; since $f(t)$ is the image of $f$ in $(I\mathrm{/}{I}^2{)}_b$ we obtain $f\equiv {\sum }_i(\mathrm{\partial }f\mathrm{/}\mathrm{\partial }{t}_i)g_i$ modulo $I_b^2$. Define the $C_b$-linear retraction $\tau \text{\hspace{0.17em}⁣}:C_b{\otimes }_P{\mathrm{\Omega }}_{P\mathrm{/}A}=(C_b{)}^m\to (I\mathrm{/}{I}^2{)}_b$ on the basis $\mathrm{d}{t}_i$ by $\tau (\mathrm{d}{t}_i)=g_i<mrow><mi\; mathvariant="normal">m</mi><mi\; mathvariant="normal">o</mi><mi\; mathvariant="normal">d</mi></mrow>I^2$. By [F6] the conormal map $\delta \text{\hspace{0.17em}⁣}:(I\mathrm{/}{I}^2{)}_b\to (C_b{)}^m$ sends the class of $f$ to ${\sum }_i(\mathrm{\partial }f\mathrm{/}\mathrm{\partial }{t}_i)\mathrm{d}{t}_i$, so the displayed congruence says exactly $\tau \circ \delta =\mathrm{i}\mathrm{d}$. Hence $\delta$ is a split injection and ${\mathrm{\Omega }}_{C_b\mathrm{/}A}\cong (C_b{)}^m\mathrm{/}\delta (I\mathrm{/}{I}^2{)}_b$ is a direct summand of the free module $(C_b{)}^m$, hence a finitely generated projective $C_b$-module by [F8].

Producing a standard smooth chart. Put $Q\subseteq P_b$ for the inverse image of $\mathfrak{q}$ and work first over the local ring $P_Q$. Let $N=(I\mathrm{/}{I}^2{)}_b{\otimes }_{C_b}\kappa (\mathfrak{q})$ and let $r={\dim }_{\kappa (\mathfrak{q})}N$. Choose $f_1,\dots ,f_r\in I_b$ whose conormal classes form a basis of $N$, and put $J=(f_1,\dots ,f_r)\subseteq P_b$. Nakayama [F7] over the local ring $(C_b{)}_{\mathfrak{q}}$ shows that these classes generate $(I\mathrm{/}{I}^2{)}_{\mathfrak{q}}$; thus $I_Q=J_Q+I_Q^2$. The finite $P_Q$-module $M=I_Q\mathrm{/}{J}_Q$ therefore satisfies $M=I_{Q}M\subseteq Q{P}_{Q}M$, so Nakayama over $P_Q$ gives $I_Q=J_Q$. The split injection $\delta$ from step 3.1 stays split after tensoring with $\kappa (\mathfrak{q})$; the chosen $f_j$ give a basis of its source, so some $r\times r$ Jacobian minor is nonzero in $\kappa (\mathfrak{q})$. Since the finitely generated ideal quotient $I_b\mathrm{/}J$ vanishes after localization at $Q$, one can invert one element outside $Q$ so that $I=J$ on that smaller chart; invert also a lift of the nonzero Jacobian minor. Then the resulting algebra is a standard smooth presentation near $\mathfrak{q}$.

Conclusion. By step 4.1, after shrinking the chart further around $\mathfrak{q}$, the finitely presented $A$-algebra $C_b$ is isomorphic to a localization of $A[t_1,\dots ,t_m]\mathrm{/}(f_1,\dots ,f_r)$ with an $r\times r$ Jacobian minor a unit, i.e. it is standard smooth at $\mathfrak{q}$ in the sense of [F5]. The pointwise criterion [F4] then shows that $A\to C_b$ is flat at $\mathfrak{q}$ with geometrically regular fibre, so $f$ is smooth at $x$ by [F2]. Since $x$ was arbitrary among the points of the chart and the charts cover $X$ (step 1.2 for the other direction, step 1.1 for the reductions), $f$ is smooth; this proves the 'if' direction.

Choice audit. The Axiom of Choice is declared in the Statement and used exactly as recorded in [F1]: through [F4], [F7] and [F8] and through the finitely many affine chart, localisation, generator and basis selections of steps 1.1, 1.2 and 4.1. The Taylor computations of steps 1.2 and 3.1 are polynomial identities and use no choice; the incompatible-axiom branch of the theory is not invoked.