Étale equals flat and unramified in finite presentation

Forward direction. Assume $f$ étale at $x$; then $f$ is smooth at $x$ and ${\mathrm{reldim}}_f(x)=0$ by [F1]. Smoothness gives flatness at $x$, local finite presentation at $x$ hence local finite type at $x$, all in [F1]. By [F2] the sheaf ${\mathrm{\Omega }}_{X\mathrm{/}S}$ is locally free near $x$ with rank ${\mathrm{reldim}}_f(x)=0$ at $x$, so its stalk at $x$ vanishes. By [F3] the morphism is unramified at $x$.

Converse, residue and fibre local ring. Assume $f$ locally of finite presentation, flat at $x$, and unramified at $x$; then $f$ is locally of finite type at $x$ and ${\mathrm{\Omega }}_{X\mathrm{/}S,x}=0$ by [F3]. Apply [F4]: $\kappa (x)\mathrm{/}\kappa (s)$ is finite separable and ${\mathfrak{m}}_s{\mathcal{O}}_{X,x}={\mathfrak{m}}_x$, so the local ring of the fibre $X_s$ at $x$ is ${\mathcal{O}}_{X,x}\mathrm{/}{\mathfrak{m}}_s{\mathcal{O}}_{X,x}={\mathcal{O}}_{X,x}\mathrm{/}{\mathfrak{m}}_x=\kappa (x)$, the field $\kappa (x)$.

Converse, geometric regularity of the fibre. Keep the hypotheses of step 1.2 and let $K\mathrm{/}\kappa (s)$ be any field extension. Write $L=\kappa (x)$, a finite separable extension of $k=\kappa (s)$. By [F5] the ring $L{\otimes }_{k}K\cong K[T]\mathrm{/}(P)$ is a product of fields, hence reduced with localisations that are fields, and by [F7] each such localisation has dimension zero. The local rings of the geometric fibre $X_s{\times }_{\mathrm{Spec}\kappa (s)}\mathrm{Spec}K$ at points over $x$ are localisations of $L{\otimes }_{k}K$, because the local ring of $X_s$ at $x$ is $L$ by step 1.2 and localisation commutes with base change; hence they are regular local rings of dimension zero. As $K$ was arbitrary, the fibre is geometrically regular at $x$ by the definition [F1].

Converse, conclusion. Under the hypotheses of step 1.2, $f$ is locally of finite presentation at $x$, flat at $x$ and has a geometrically regular fibre at $x$ by step 2.1, so $f$ is smooth at $x$ by [F1]. Moreover the local rings of the geometric fibre over $x$ are products-of-fields localisations of dimension zero (step 2.1), so the relative dimension of $f$ at $x$ is $0$ in the sense of [F1]; by [F1] again, $f$ is étale at $x$.

Conclusion and accounting. Step 1.1 proves that étale at $x$ implies flat and unramified at $x$, and steps 1.2, 2.1 and 3.1 prove the converse, so étale $=$ flat $+$ unramified for locally finitely presented morphisms. The vanishing-differential input is tested on affine charts via [F6]. The Axiom of Choice [F8] is assumed in the Statement and is used exactly through [F2] and [F4], and through the field-theoretic suppliers of [F5]; no other selection occurs. [F2, F4, F5, F6, F8, step 1.1, step 3.1] $\mathrm{\square }$