# The local nature of formal smoothness and an apparently extraneous hypothesis of finite presentation

In showing that formal smoothness is a local property, EGA seems to use the following presentation (and in fact, seems to contain a mistake according to this question). The proposition is as follows:

Proposition (EGA$$\ IV_{4}, 16.5.18)$$: Suppose $$X,Y$$ are schemes over $$S$$ and $$Y_0$$ is a closed subscheme of $$Y$$ defined by the ideal sheaf $$\mathscr I$$ that is square $$0$$. Assume also that $$Y$$ is affine and $$\Omega^1_{X/S}$$ is finitely presented.

We are given a map $$u_0: Y_0 \to X$$. Then, if $$U_\alpha$$ is an open cover of $$X$$ and we can lift $$u_0$$ locally to maps $$u_\alpha$$ defined on the appropriate open subsets of $$Y$$, we can find a global lift $$u: Y\to X$$.

My understanding of this proof is as follows. They show that the sheaf $$\mathscr P$$ on $$Y$$ defined by $$\Gamma(V,\mathscr P) = \{f: V \to X: f_0 = u_0: V/\mathscr I \to X\}$$ is a torsor of the sheaf $$\mathscr G = \mathcal{Hom}_{Y_0}(u_0^{*}\Omega_{X/S}, \mathscr I)$$ and since $$Y_0$$ is affine, $$\mathscr P$$ is the trivial torsor. Then, the $$0$$ section of $$\mathscr G$$ gives the required lift.

Question: Assuming my outline of the argument above is correct, where does the finite presentation of $$\Omega_{X/S}$$ get used?