Following this thread, I'm trying to prove in detail this theorem. Could you please check if my proof is fine or contains logical mistakes?
Theorem: Let $X \subseteq \mathbb R^M$ and $Y \subseteq \mathbb R^N$ be $n$-dimensional smooth manifolds, $f:X \to Y$ smooth, and $x \in X$. If $\mathrm d f_x: T_x X \to T_{f(x)}Y$ is an isomorphism, then $f$ is a local diffeomorphism around $x$.
Proof: Clearly, $T_xX$ and $T_{f(x)}Y$ are $n$-dimensional vector subspace of $\mathbb R^M$ and $\mathbb R^N$ respectively. Let $\varphi:U \to V$ and $\psi:A \to B$ be local parameterizations around $x$ and $f(x)$ respectively.
Clearly, $f \circ \varphi$ is smooth. There exists an open neighborhood $U'$ of $\varphi^{-1} (x)$ in $U$ such that $h:= \psi^{-1} \circ f \circ \varphi_{\restriction U'}$ is well-defined, i.e., the domains and images of functions in the composition are compatible.
Clearly, $h$ is smooth and we write $$\mathrm d h_{\varphi^{-1} (x)}: \mathbb R^n \to \mathbb R^n.$$
Also, $$\mathrm d f_x := \mathrm d \psi_{\psi^{-1} \circ f (x)} \circ \mathrm d h_{\varphi^{-1} (x)} \circ (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1}.$$
Because $\varphi, \psi$ are diffeomorphisms, $$\mathrm d \psi_{\psi^{-1} \circ f (x)}: \mathbb R^n \to T_{f(x)}Y \quad \text{and} \quad (\mathrm d \varphi_{\varphi^{-1} (x)})^{-1}: T_x X \to \mathbb R^n$$ are isomorphisms. This combining with the fact that $\mathrm d f_x$ is an isomorphism implies $\mathrm d h_{\varphi^{-1} (x)}$ is also an isomorphism.
Notice that $h$ is a smooth function whose domain is an open subset of a Euclidean spaces, so we can apply IFT for Banach spaces. This means there exists an open neighborhood $U''$ of $\varphi^{-1} (x)$ in $U'$ such that $A' := h(U'')$ is open in $\mathbb R^n$, and $h_{\restriction U''}: U'' \to A'$ is a diffeomorphism. Wlog, we assume $U' = U''$.
There exists some open neighborhood $V'$ of $x$ in $V$ such that $f_{\restriction V'} = \psi \circ h \circ \varphi^{-1}_{\restriction V'}$ is well-defined, i.e., the domains and images of functions in the composition are compatible. Diffeomorphism is open, so we can take, for example, $V' := \varphi (U')$.
We have $\varphi^{-1}_{\restriction V'}$, $h$, and $\psi$ are all diffeomorphisms, so $f_{\restriction V'}: V' \to B'$ with $B' := f(V')$ is the composition of diffeomorphisms and thus is also a diffeomorphism.
We have $V'$ is open in $V$ and $V$ is open in $X$, so $V'$ is open in $X$ by this lemma. Let's show that $B'$ is indeed open in $Y$.
First, $V'$ is open in $V$ and $\varphi^{-1}: V \to U$ is a diffeomorphism implies $\varphi^{-1} (V')$ is open in $U$. This combining with this lemma and $\varphi^{-1} (V') \subseteq U' \subseteq U$ implies $\varphi^{-1} (V')$ is open in $U'$.
Second, $h:U' \to A'$ is a diffeomorphism, so $h \circ \varphi^{-1} (V')$ is open in $A'$. On the other hand, $A'$ is open in $A$, so $h \circ \varphi^{-1} (V')$ is open in $A$ by this lemma.
Third, $\psi: A \to B$ is a diffeomorphism, so $B'$ is open in $B$. On the other hand, $B$ is open in $Y$, $B'$ is also open in $Y$ be this lemma.