Redundance of the Smoothness of the Inversion Map in the Definition of a Lie Group. $\DeclareMathOperator{\inv}{inv}$
I am trying to understand the proof of the following from this document:

Let $M$ be a smooth manifold which admits a group structure such that the multiplication map $m:G\times G\to G$ defined as $m(g, h)=gh$ for all $g, h\in G$ is a smooth map.
Then the inversion map $\inv:G\to G$ defined as $\inv(g)=g^{-1}$ for all $g\in G$ is a smooth map.

The proof in the document proceeds as follows:
First note that the multiplication map is a constant rank surjective smooth map, and is therefore a submersion. Therefore, the level set $\Delta=m^{-1}(e)$ of $e\in G$, $e$ being the identity of the group structure, is an embedded submanifold of $G\times G$ of dimension $n$.
Now let $\pi_1:G\times G\to G$ be the projection on the first coordinate.
Consider the map $\pi_1\circ i:\Delta\to G$, where $i:\Delta\to G\times G$ is the inclusion map, which we know is a smooth embedding.
It is claimed in the document that $\pi_1\circ i$ is a diffeomorphism.
The reasoning given seems to be this: The map $\pi_1\circ i$ is smooth and is a homeomorphism and hence by the inverse function theorem, it is also a diffeomorphism.
This seems to suggest that any smooth homeomorphism is a diffeomorphism. But this is not true since the map $x\mapsto x^3:\mathbf R\to \mathbf R$ is a smooth topological embedding but not an immersion at $x=0$.
How do I show that that composition $\pi_1\circ i$ is a diffeomorphism?
 A: Here is perhaps a more straightforward proof of your statement. We can realize the inversion as the composition $\mathrm{inv}=\mathrm{pr_2}\circ F^{-1}\circ \iota$, where we have defined $\iota\colon G\rightarrow G\times G$ as $\iota(g)=(g,e)$ and
$$F\colon G\times G\rightarrow G\times G,\quad F(g,h)=(g,gh).$$
Note that the map $F$ is a smooth bijection with inverse $(g,k)\mapsto(g,g^{-1}k)$, so we would like to show it's a diffeomorphism. By dimensionality and inverse map theorem, it's enough to show it's an immersion at all points.
Suppose $\mathrm d F_{(g,h)}(v,w)=0$ for some $(v,w)\in T_gG\oplus T_hG$. Since $\mathrm{pr}_1=\mathrm{pr}_1\circ F$, we get $\mathrm d(\mathrm{pr}_1)_{(g,h)}(v,w)=0$ and hence $v=0$. To prove that $w=0$, we consider the equality $m=\mathrm{pr}_2\circ F$, where $m$ denotes the multiplication map; differentiating it yields $\mathrm d m_{(g,h)}(v,w)=0$. On the other hand,
$$
\mathrm d m_{(g,h)}(v,w)=\mathrm d(L_g)_h(w)+\mathrm d(R_h)_g(v)=\mathrm d(L_g)_h(w),
$$
hence $\mathrm d(L_g)_h(w)=0$, implying $w=0$ since $L_g$ is a diffeomorphism. So $F$ is an immersion at $(g,h)\in G\times G$.
A: You are right, the argument isn't conclusive, it's missing a piece, but it's fixable. You need to note that the map $p_1=\pi_1\circ\iota:\Delta'\to G$ has constant rank equal to $\dim G=\dim\Delta'$.

Indeed, let $m=(g,g^{-1})\in\Delta'$ be a point in $\Delta'$, then 
\begin{array}{cccc}
\theta_g&:&G\times G&\longrightarrow & G\times G\\
&&(x,y) & \longmapsto &(gx,yg^{-1})
\end{array}
is a diffeomorphism of $G\times G$ and sends $\Delta'$ diffeomorphically to itself (let's call $\widetilde{\theta_g}$ the induced diffeomorphism of $\Delta'$). Then $$p_1\circ\widetilde{\theta_g}=\pi_1\circ\iota\circ\widetilde{\theta_g}=\pi_1\circ\theta_g\circ\iota=L_g\circ\pi_1\circ\iota=L_g\circ p_1$$ (where $L_g$ is left multiplication by $g$). If we calculate the differentials at $m_0=(e,e)\in\Delta'$, we get
$$d_{m}p_1\circ d_{m_0}\widetilde{\theta_g}=d_eL_g\circ d_{m_0}p_1 $$
Since $\widetilde{\theta_g}$ and $L_g$ are diffeomorphisms, $p_1$ has the same rank at $m\in\Delta'$ as at $m_0\in\Delta'$, so that it has constant rank ($\leq\dim G$). It follows from the constant rank theorem (see the first theorem in these notes) and the bijectivity of $p_1$, that $p_1$ has constant rank equal to $\dim G$, and now you can apply the global inversion theorem.
