$$ \newcommand{\wh}{\widehat} \newcommand{\R}{\mathbf R} \newcommand{\mr}{\mathscr} \newcommand{\set}[1]{\{#1\}} \newcommand{\inclusion}{\hookrightarrow} \newcommand{\vp}{\varphi} $$
I am trying to understand the following theorem:
Theorem. Let $M$ be a smooth manifold and $S$ be a subset of $M$. There is a unique smooth structure on $S$, if one exists, which makes it into a smooth manifold such that $i:S\inclusion M$ is a smooth embedding.
The only way I could prove this is via the lemma proved below whose proof is very long. I think the proof of the above theorem should be fairly straightforward and clear and should not require to do what I have done. Does somebody have a short proof?
Lemma. Let $S$ be a $k$-dimensional embedded submanifold of a smooth manifold $M$. Then for each $p\in S$, there exist a smooth charts $(U_p, \vp_p)$ and $(V_p, \psi_p)$ about $p$ on $S$ and $M$ respectively such that $U_p=V_p\cap S$, and $\psi_p\circ\vp_p^{-1}:\wh U_p\to \wh V_p$ (the `hat' denotes the image of the open set under the corresponding chart) \begin{equation*} \psi_p\circ\vp_p^{-1}(x_1 , \ldots, x_k) = (x_1 , \ldots, x_k, 0 , \ldots, 0) \end{equation*} for all $(x_1 , \ldots, x_k)\in \wh U_p$. Therefore $\vp_p=(\pi\circ \psi_p\circ i)|_{V_p\cap S}$, where $\pi:\R^n\to \R^k$ is the projection on the first $k$ coordinates, and the collection of smooth charts $\mr U=\set{V_p\cap S,\ (\pi\circ \psi_p\circ i)|_{V_p\cap S}}_{p\in S}$ is a smooth atlas on $S$.
Proof:
Since $i:S\inclusion M$ is an immersion (it's more than that), by the Constant Rank Theorem, we know that there exists a smooth chart $(U,\vp)$ on $S$ containing the point $p$, and a smooth chart $(V,\psi)$ on $M$, again containing $p$, such that $U\subseteq V$ and $\psi\circ\vp^{-1}(x_1,\ldots,x_k)=(x_1,\ldots,x_k,0,\ldots,0)$ for all $(x_1,\ldots,x_k)\in \wh U$.
Since $i:S\inclusion M$ is in particular a topological embedding, we know that $U$ is open in $M$ and thus we may WLOG assume that $U=V\cap S$.
We now show that $\vp=(\pi\circ \psi\circ i)|_{V\cap S}$.
For take $q\in V\cap S$, and say $\vp(q)=(x_1 , \ldots, x_k)$.
Now we have $\psi\circ \vp^{-1}(x_1 , \ldots, x_k)=(x_1, , \ldots, x_k, 0 , \ldots, 0)$, giving $(\pi\circ \psi\circ i)(q)=(x_1 , \ldots, x_k)$.
So we have shown that for each $p\in S$, there exist a smooth charts $(U_p, \vp_p)$ and $(V_p, \psi_p)$ about $p$ on $S$ and $M$ respectively such that $U_p=V_p\cap S$, and $\psi_p\circ\vp_p^{-1}:\wh U_p\to \wh V_p$ \begin{equation*} \psi_p\circ\vp_p^{-1}(x_1 , \ldots, x_k) = (x_1 , \ldots, x_k, 0 , \ldots, 0) \end{equation*} for all $(x_1 , \ldots, x_k)\in \wh U_p$. It remains to show that $\mr U=\set{U_p, \vp_p}_{p\in S}$ is a smooth atlas on $S$. To see this, consider note that \begin{equation*} \vp_q\circ \vp_p^{-1} = \vp_q\circ \psi_p^{-1} \circ \psi_p\circ \vp_p^{-1} \end{equation*} and this map sends $(x_1 , \ldots, x_k)$ to $\pi\circ\psi_q^{-1}\circ\psi_p(x_1 , \ldots, x_k, 0 , \ldots, 0)$ for all $(x_1 , \ldots, x_k)\in \vp_p(U_p\cap U_q)$, and hence is smooth.