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?