Solution (source code)

= Solution

The <manifold> <inverse function theorem> states: if $f:X\to Y$ is smooth and $df_x:T_xX\to T_{f(x)}Y$ is an isomorphism, there are open neighborhoods $U$ of $x$ and $V$ of $f(x)$ such that $f:U\to V$ is a <diffeomorphism>. In particular the <manifolds> have the same dimension at those points.

Choose charts $\phi$ around $x$ and $\psi$ around $f(x)$, shrinking the source chart so its image under $f$ lies in the target chart. The coordinate map $F=\psi\circ f\circ\phi^{-1}$ has <derivative> $d\psi\circ df_x\circ d\phi^{-1}$, an invertible <matrix>. Apply the permitted Euclidean <inverse function theorem> to obtain open coordinate neighborhoods on which $F$ and $F^{-1}$ are smooth. Pull them back through the charts. The resulting inverse is $\phi^{-1}\circ F^{-1}\circ\psi$, smooth by composition. This proves the <manifold> statement.