Based on Possible formal smoothness mistake in EGA, let $X$ and $Y$ $k$-schemes ($k$ a field),
let $f:X\rightarrow Y$ a fpqc morphism such that $f$ is formally smooth and $X$ formally smooth, do we have $Y$ formally smooth?
We can already show that $\Omega_{Y/k}^{1}$ is locally projective.
As a matter of fact, from the classic exact sequences and as $f$ and $X$ are formally smooth, we deduce first that:
$f^{*}\Omega_{Y/k}^{1}$ is locally projective and then using Raynaud -Gruson, we know that local projectivity is a fpqc local condition so $\Omega_{Y/k}^{1}$ is locally projective.
Then, using the criterion given in Possible formal smoothness mistake in EGA, we only have to prove that $N_{Y/k}=0$.
Is it true in this case?