This question is a follow-up to Identity up to isomorphism treated as identity in proof. I thought that with all the kind help given there, now I would be able to work out the sketch of a proof given by Lang for the corollary dual to the one in the above thread, and to eliminate his assumptions of identity based on an identity up to isomorphism there, too. But I can't. Here is the problem:
In "Fundamentals of Differential Geometry", 1999, pp.18-19, Serge Lang gives the following definition:
And then this corollary to the inverse mapping theorem:
First of all, some clarifications: Morphism means $ C^p$ map, local isomorphism means local $ C^p$ diffeomorphism, toplinear isomorphism can be considered to be a linear isomorphism here. Furthermore, I understand to be $ V_1 \subseteq E_1 $ and $ V_2 \subseteq E_2 $, and the local inverse h, which Lang refers to, to be $ \varphi^{-1} $, and not the inverse of the derivative, as Lang's wording implies.
Again, what I don't see is how $ \varphi^{-1} $ satisfies the requirement of the corollary.
In order to eliminate the identification $ E_2=F $ in the proof, let instead be
$ \varphi: E_1 \times E_2 \rightarrow E_1 \times F $.
Then introduce the $ C^p $ diffeomorphism
$ g: E_1 \times E_2 \rightarrow E_1 \times F: \quad (x_1,x_2) \mapsto (id_1, D_2f(a_1,a_2))[x_1,x_2] $
and replace $ h:=\varphi^{-1} $ by the $ C^p $ diffeomorphism $ h \circ g: E_1 \times E_2 \rightarrow E_1 \times E_2 $. But with this, how does the resulting map $ f \circ h \circ g: E_1 \times E_2 \rightarrow F $ factor into an ordinary projection $ V_1 \times V_2 \rightarrow V_2 $ and a linear isomorphism $ V_2 \rightarrow W(0) \subseteq F $ with an open neighborhood W?
Can we state the local map $ \varphi^{-1} $ explicitly? Is it $ \varphi^{-1}(x_1,y) = (x_1, pr_2 \circ f^{-1}(y)) $ for $ y \in F $?
Clearly $ \varphi^{-1}(\varphi(x_1,x_2))= \varphi^{-1}(x_1,f(x_1,x_2)) = (x_1,x_2) $. But the other way around does not resolve properly:
$ \varphi(\varphi^{-1}(x_1,y))= \varphi(x_1, pr_2 \circ f^{-1}(y)) =(x_1,f(x_1,pr_2 \circ f^{-1}(y)) $.
And by the way, can we take f to be locally invertible, too? Evaluating the composition $ f \circ h \circ g $ seems to lead nowhere
$ f(h(g(x_1,x_2))) = f(h(x_1,D_2f(a_1,a_2)[x_2])) = f(x_1,pr_2 \circ f^{-1}(D_2f(a_1,a_2)[x_2])) $.
So, how to proceed? Where is the error, or what is the necessary idea? I thought about explicitly introducing the projection $ pr_2: E_1 \times E_2 \rightarrow E_2 \equiv (\{0\} \times E_2) \subseteq (E_1 \times E_2) $ at the beginning of the composition: $ f \circ h \circ g \circ pr_2 $, but unfortunately the projection is no $ C^p $-diffeomorphism.
In this case it is much easier to get lost.
If we go through the proof lets redefine $$\varphi:U\to E_1\times F, \quad (x,y)\mapsto (x,f(x,y))$$ this is also a bit different from what Lang is doing in that $\varphi$ is not defined on the entire space $E_1\times E_2$, since $f$ itself is only defined on the neighbourhood $U$. This remark is far from serious, however.
The derivative of this is: $$D\varphi(x,y)\ [w_1,w_2]= \bigg[w_1, D_1f(x,y)\ [w_1] + D_2f(x,y)\ [w_2]\bigg]$$
This is invertible at $(a_1,a_2)$. You may use matrix notation, as Lang does, to simplify this - note that for $A, C$ invertible you have that $$\begin{pmatrix}A&0\\ B& C\end{pmatrix}^{-1}= \begin{pmatrix}A^{-1}&0\\ -C^{-1}BA^{-1}& C^{-1}\end{pmatrix}$$
From the inverse function theorem it follows that there is some local inverse $$h: V_1\times V_2\to E_1\times E_2$$ with $V_1\subseteq E_1, V_2\subseteq F$ open so that $\varphi(a_1,a_2)\in V_1\times V_2$ (and $h(V_1\times V_2)\subseteq U$).
Since its a local inverse you have $\varphi \circ h=\mathrm{id}_{V_1\times V_2}$. Write this composition out: $$(\varphi\circ h)(x,y)=(h_1(x,y), f(h(x,y)) ) \overset!= (x,y)$$ hence $f(h(x,y)) = y$, which was the desired result.
What I did here was go through the proof and adapt it to be a proof of the statement without assuming that $E_2=F$. From reading your thoughts I think you wanted to do the same thing, but as an adaption you want to plug in the isomorphism $D_2f(a_1,a_2)$ at every stage where the identification takes place. This is also possible, and maybe its more systematic, but its easier to get lost.
A third way to do it would be to use the actual statement derived by Lang, meaning the case $E_2=F$, and work with this statement alone to derive the case $E_2\neq F$. Here we need to first use the identifications to get the situation $E_2=F$, then apply the theorem and after that use identifications to get back to the situation $E_2\neq F$.
In this vain let $T:F\to E_2$ be any isomorphism, for example $T=D_2f(a_1,a_2)^{-1}$. Then if $$f:U\to E_1\times F$$ is a map with $D_2f(a_1,a_2)$ being invertible consider $\tilde f:=f\circ (\mathrm{id}_{E_1}, T): E_1\times F\to E_1\times F$. Here we have modified $f$ to be a map of the required form, note that $$D_2\tilde f = D_2f(a_1,a_2)\circ T$$ which is invertible - you are thus in the situation of the lemma where $E_2=F$.
Apply the theorem: There exists a $\tilde h:V_1\times V_2\to E_1\times F$ so that $\tilde f \circ \tilde h$ is a projection to the second component. But: $$\tilde f\circ \tilde h = f\circ ( (\mathrm{id}_{E_1},T)\circ \tilde h)$$ Defining $h:= (\mathrm{id}_{E_1},T)\circ \tilde h$ then allows you to recover the lemma where you just have $E_2\cong F$, rather than the full $E_2=F$.