[proofplan]
Let $G := F^{-1}$ denote the inverse diffeomorphism. The identities $G \circ F = \operatorname{id}_M$ and $F \circ G = \operatorname{id}_N$ imply, after applying the [chain rule for differentials](/theorems/3907), that $dG_{F(p)}$ is both a left and right inverse for $dF_p$. Since the differential of an identity map is the identity map on the corresponding tangent space, these two identities prove that $dF_p$ is a linear isomorphism and that its inverse is exactly $d(F^{-1})_{F(p)}$.
[/proofplan]
[step:Introduce the inverse diffeomorphism and the relevant tangent maps]
Fix $p \in M$. Since $F: M \to N$ is a diffeomorphism, its inverse is a smooth map
\begin{align*}
G := F^{-1}: N \to M.
\end{align*}
Define the two linear maps
\begin{align*}
L := dF_p: T_pM \to T_{F(p)}N
\end{align*}
and
\begin{align*}
K := dG_{F(p)}: T_{F(p)}N \to T_pM.
\end{align*}
We will prove that $K = L^{-1}$.
[/step]
[step:Differentiate the two inverse identities]
Because $G = F^{-1}$, the compositions satisfy
\begin{align*}
G \circ F = \operatorname{id}_M
\end{align*}
as maps $M \to M$, and
\begin{align*}
F \circ G = \operatorname{id}_N
\end{align*}
as maps $N \to N$.
Apply the chain rule for differentials to $G \circ F$ at the point $p$. Both maps are smooth: $F$ is smooth because it is a diffeomorphism, and $G$ is smooth by the definition of diffeomorphism. Hence
\begin{align*}
d(G \circ F)_p = dG_{F(p)} \circ dF_p.
\end{align*}
Since $G \circ F = \operatorname{id}_M$, and the differential of the identity map on $M$ at $p$ is $\operatorname{id}_{T_pM}$, we obtain
\begin{align*}
K \circ L = \operatorname{id}_{T_pM}.
\end{align*}
Now apply the chain rule for differentials to $F \circ G$ at the point $F(p) \in N$. Since $G(F(p)) = p$, the chain rule gives
\begin{align*}
d(F \circ G)_{F(p)} = dF_{G(F(p))} \circ dG_{F(p)} = dF_p \circ dG_{F(p)}.
\end{align*}
Since $F \circ G = \operatorname{id}_N$, and the differential of the identity map on $N$ at $F(p)$ is $\operatorname{id}_{T_{F(p)}N}$, we obtain
\begin{align*}
L \circ K = \operatorname{id}_{T_{F(p)}N}.
\end{align*}
[guided]
The reason to introduce $G := F^{-1}$ is that the inverse-map relation is expressed by two exact identities of smooth maps:
\begin{align*}
G \circ F = \operatorname{id}_M
\end{align*}
and
\begin{align*}
F \circ G = \operatorname{id}_N.
\end{align*}
These identities are stronger than pointwise inverse relations; they can be differentiated.
First consider $G \circ F: M \to M$ at the point $p \in M$. The chain rule for differentials applies because $F$ and $G$ are smooth maps. It gives
\begin{align*}
d(G \circ F)_p = dG_{F(p)} \circ dF_p.
\end{align*}
But $G \circ F$ is the identity map on $M$. The differential of the identity map at $p$ is the identity [linear map](/page/Linear%20Map) on $T_pM$, so
\begin{align*}
dG_{F(p)} \circ dF_p = \operatorname{id}_{T_pM}.
\end{align*}
With the abbreviations $L := dF_p$ and $K := dG_{F(p)}$, this says
\begin{align*}
K \circ L = \operatorname{id}_{T_pM}.
\end{align*}
This proves that $K$ is a left inverse for $L$. To know that $K$ is the actual inverse of $L$, we also verify the opposite composition. Apply the chain rule to $F \circ G: N \to N$ at $F(p) \in N$. Since $G(F(p)) = p$, we get
\begin{align*}
d(F \circ G)_{F(p)} = dF_{G(F(p))} \circ dG_{F(p)} = dF_p \circ dG_{F(p)}.
\end{align*}
The map $F \circ G$ is the identity map on $N$, so its differential at $F(p)$ is $\operatorname{id}_{T_{F(p)}N}$. Therefore
\begin{align*}
dF_p \circ dG_{F(p)} = \operatorname{id}_{T_{F(p)}N}.
\end{align*}
Equivalently,
\begin{align*}
L \circ K = \operatorname{id}_{T_{F(p)}N}.
\end{align*}
Thus $K$ is both a left inverse and a right inverse for $L$.
[/guided]
[/step]
[step:Identify the inverse linear map]
The identities
\begin{align*}
K \circ L = \operatorname{id}_{T_pM}
\end{align*}
and
\begin{align*}
L \circ K = \operatorname{id}_{T_{F(p)}N}
\end{align*}
show that $L$ is a linear isomorphism with inverse $K$. Substituting back the definitions of $L$ and $K$, this says that
\begin{align*}
dF_p: T_pM \to T_{F(p)}N
\end{align*}
is a linear isomorphism and
\begin{align*}
(dF_p)^{-1} = dG_{F(p)} = d(F^{-1})_{F(p)}.
\end{align*}
Since $p \in M$ was arbitrary, the conclusion holds for every $p \in M$.
[/step]
