The smooth inverse function theorem on manifolds

Choose smooth charts $(U_0,\phi )$ at $p$ and $(V_0,\psi )$ at $F(p)$ as in [L4], and let $f:=\psi \circ F\circ {\phi }^{-1}$. By [L4], the chart maps ${\phi }^{-1}$ and $\psi$ are diffeomorphisms, so their differentials are linear isomorphisms. Applying [L1] gives $Df(\phi (p))=d{\psi }_{F(p)}\circ d{F}_p\circ d({\phi }^{-1}{)}_{\phi (p)}\mathrm{.}$ Because $d{F}_p$ is an isomorphism by [F1], the Euclidean differential $Df(\phi (p))$ is invertible.

By [L2], after shrinking to open neighbourhoods $\tilde{U}\subseteq \phi (U_0)$ and $\tilde{V}\subseteq \psi (V_0)$ of $\phi (p)$ and $\psi (F(p))$, the restriction $f\mathrm{\mid }\tilde{U}:\tilde{U}\to \tilde{V}$ is a bijection with $C^1$ inverse. Since $f$ is smooth, [L3] upgrades that inverse to a smooth one.

Put $U:={\phi }^{-1}(\tilde{U})$ and $V:={\psi }^{-1}(\tilde{V})$. Then $F{\mathrm{\mid }}_U={\psi }^{-1}\circ (f\mathrm{\mid }\tilde{U})\circ \phi$, so $F{\mathrm{\mid }}_U:U\to V$ is bijective. Its inverse is ${\phi }^{-1}\circ (f\mathrm{\mid }\tilde{U}{)}^{-1}\circ \psi$, which is smooth by [L4] and step 2.1.

Thus $F{\mathrm{\mid }}_U$ is a bijective smooth map with smooth inverse, hence a diffeomorphism of neighbourhoods.