Hartshorne Theorem 8.17 I can't understand the proof of theorem 8.17 from Hartshorne's "Algebraic Geometry". Namely, he says that we have an exact sequence 
$$
0 \to \mathcal J'/\mathcal J'^2 \to \Omega_{X/k} \otimes \mathcal O_{Y'} \to \Omega_{Y'/k} \to 0 
$$
and there are $x_1, \dots,x_r$ such that $dx_1, \dots, dx_r$ generate a free subsheaf of rank $r$ in a neighborhood of $y \in Y$. It follows that $\Omega_{Y'/k}$ is locally free. Why?
 A: Here's one possible proof I had in mind. Kindly point out if there is any error. 
Assume $Y$ is a non-singular algebraic variety of dimension $s$ with quasi-coherent ideal sheaf given by $\mathscr I$. Then $\Omega^1_{Y,k}$ is a locally free sheaf of rank $s$. We consider the second fundamental exact sequence $$\mathscr I/\mathscr I^2\xrightarrow{\delta}\Omega^1_{X,k}\otimes_{\mathcal O_X} \mathcal O_y\xrightarrow{u} \Omega^1_{Y,k}\rightarrow 0$$ $$\implies \mathscr I_y/\mathscr I_y^2\xrightarrow{\delta}\Omega^1_{X/k,y}\otimes_{\mathcal O_{X,y}} \mathcal O_{Y,y}\xrightarrow{u} \Omega^1_{Y/k,y}\rightarrow 0$$ is exact where $y$ is a closed point. let $U=Spec \ R$ be an affine open neighbourhood of $y$ in $X$. So $U\cap Y$ is also affine and irreducible since $Y$ is. So $U\cap Y=V(P)$ where $P\in Spec \ R$ i.e. we have $\mathscr I(U)=P$.  Thus we get as $Y\cap U$ is non-singular $PR_P/P^2R_P=\left (\frac{P}{P^2} \right )_P$ is a free $R_P/PR_P$ module of rank $\dim R_P=\mathrm {ht} \ P=n-s=r$ and hence $\exists f\not \in P$ such that $PR_f/P^2R_f$ is free of rank $r$. Thus we get $\mathscr I/\mathscr I^2$ is locally free of rank $r$. Thus we get from $$\mathscr I_y/\mathscr I_y^2\xrightarrow{\delta}\Omega^1_{X/k,y}\otimes_{\mathcal O_{X,y}} \mathcal O_{Y,y}\xrightarrow{u} \Omega^1_{Y/k,y}\rightarrow 0$$ the left most map is injective as well since all the modules are free of finite rank. We know $Ker \ u$ is free of rank $r$ at $y$ and so is $\mathscr I_y/\mathscr I_y^2$. Also $\delta$ is a surjection from latter to the former and hence an isomorphism by an application of Nakayama's lemma.  So we get the exact sequence $$0\rightarrow \mathscr I/\mathscr I^2\rightarrow \Omega^1_{X/k}\otimes_{\mathcal O_X} \mathcal O_Y\rightarrow \Omega^1_{Y/k}\rightarrow 0$$
A: I want to propose an alternative for verifying that the relative conormal sequence is exact in the case of a nonsingular subvariety of a nonsingular variety.
The question is local, and so we are in the setting of Proposition 16.12 in Eisenbud.

Proposition 16.12 (Eisenbud): If $\pi:S\rightarrow T$ is an epimorphism of $R$-algebras, with kernel $I$, then in the conormal sequence
  $$I/I^2\xrightarrow{d}T\otimes_S\Omega_{S/R}\xrightarrow{D\pi}\Omega_{T/R}\rightarrow0$$
  the map $d$ is a split injection iff there is a map of $R$-algebras $\tau:T\rightarrow S/I^2$ splitting the projection map $S/I^2\twoheadrightarrow S/I=T$.

In fact, EGA IV Th. 20.5.12 establishes a canonical bijection between left inverses of $d$ and morphisms $\tau$. 
Hence to achieve left-exactness of the relative conormal sequence, it is sufficient to establish the existence of such a map $\tau$. Hartshorne discusses the existence of a more general map in ex. II.8.6 under the title The Infinitesimal Lifting Property, but the vocabulary formally smooth is developed in EGA.

EGA IV Déf. 19.3.1 A morphism of algebras $A\rightarrow B$ is formally smooth (for the discrete topology) if, for all $A$-algebra $C$ and all nilpotent ideal $\mathfrak I$ of $C$, every $A$-homomorphism $u:B\rightarrow C/\mathfrak I$ factors as $B\xrightarrow{v}C\xrightarrow{\varphi}C/\mathfrak I$, where $\varphi$ is the canonical epimorphism. ($\Rightarrow$ $C$ satisfies the the infinitesimal lifting property.)

You will notice that in the Hartshorne ex. II.8.6, it is proved that if $A=k=k^{\mathrm{alg}}$ and $C$ is a finitely-generated $A$-algebra such that the associated affine scheme is nonsingular/$k$, then $C$ has the infinitesimal lifting property. Taking $R=k$, $B=S/I$, $C=S/I^2$, and $u$ the identity, we would establish the existence of a desired map $\tau$ and verify the left-exactness of the relative conormal sequence provided we could show that if $I$ corresponds to a nonsingular subvariety, $C=S/I^2$ has the infinitesimal lifting property. The Hartshorne ex. II.8.6 does this for us, but unfortunately it uses the result we are trying to prove. So instead, certainly it would suffice to show that for varieties, nonsingular implies formally smooth.
EGA IV defines (17.3.1) a morphism to be smooth if it is formally smooth and of locally finite presentation; since we are considering a morphism of varieties, a morphism is defined to be smooth if it is formally smooth. The notion of smooth morphism $A\rightarrow B$ is local on both (Rem. 17.3.2), and it is the same to say that a morphism is smooth, or that it is smooth at every point of the source (scheme).
We conclude with the desired remark, namely that a variety/$k$ is formally smooth iff it is a nonsingular variety. This is the content of EGA IV Cor. 17.5.2.
A: Let $i:Y\to X.$ As in the book proof, one starts with some neighborhood of $y\in Y$ to make all sheaves under consideration free.
Then
$$
i^*\Omega_{X/k} = \Omega_{X/k} \otimes \mathcal O_{Y}=\ker \phi \oplus \Omega_{Y/k}
$$
because $\Omega_{Y/k}$ is locally free (projective) sheaf, hence it is a direct summand. Thus $\ker \phi$ is also projective (and locally free).
As $\Omega_{X/k}$ splits at the point $y,$ it splits in some neighborhood of $y$ with one of summands equal to $(dx_1, \dots, dx_r)$, where $(dx_1, \dots, dx_r)\otimes\mathcal O_{Y} = \ker\phi$:
$$
\Omega_{X/k} = (dx_1, \dots, dx_r) \oplus M.
$$
$M$ sheaf is locally free as direct summands of locally free $\Omega_{X/k}$.
Pull back to $Y'$:
$$
\Omega_{X/k} \otimes \mathcal O_{Y'} = (dx_1, \dots, dx_r) \otimes \mathcal O_{Y'} \oplus M\otimes\mathcal O_{Y'},
$$
where $\mathcal {J'}/\mathcal {J'^2} \cong (dx_1, \dots, dx_r) \otimes \mathcal O_{Y'}$ and $M\otimes\mathcal O_{Y'} = \Omega_{X/k} \otimes \mathcal O_{Y'}/(\mathcal {J'}/\mathcal {J'^2})=\Omega_{Y'/k}$, using  sequence from question.
Thus $\Omega_{Y'/k}$ is locally free as direct summand.
