[proofplan]
Let $G: N \to M$ denote the smooth inverse map $F^{-1}$. Since $G \circ F = \operatorname{id}_M$ and $F \circ G = \operatorname{id}_N$, the [chain rule for differentials](/theorems/3907) turns these two identities of smooth maps into two identities of linear maps on tangent spaces. These identities show that $dG_{F(p)}$ is both a left and right inverse for $dF_p$, so $dF_p$ is a linear isomorphism.
[/proofplan]
[step:Introduce the smooth inverse and the relevant tangent maps]
Fix a point $p \in M$, and define $q := F(p) \in N$. Since $F: M \to N$ is a diffeomorphism, it is bijective, smooth, and its inverse map
\begin{align*}
G := F^{-1}: N \to M
\end{align*}
is smooth. The differential of $F$ at $p$ is the [linear map](/page/Linear%20Map)
\begin{align*}
dF_p: T_pM \to T_qN.
\end{align*}
The differential of $G$ at $q$ is the linear map
\begin{align*}
dG_q: T_qN \to T_{G(q)}M.
\end{align*}
Because $q = F(p)$ and $G = F^{-1}$, we have $G(q) = p$, so this becomes
\begin{align*}
dG_q: T_qN \to T_pM.
\end{align*}
[/step]
[step:Apply the chain rule to the two inverse identities]
The inverse identities for $F$ and $G$ are
\begin{align*}
G \circ F = \operatorname{id}_M
\end{align*}
and
\begin{align*}
F \circ G = \operatorname{id}_N.
\end{align*}
Both compositions are smooth because $F$ and $G$ are smooth. Applying the chain rule for differentials to $G \circ F: M \to M$ at $p$ gives
\begin{align*}
d(G \circ F)_p = dG_{F(p)} \circ dF_p.
\end{align*}
Since $G \circ F = \operatorname{id}_M$, the differential of the left-hand side is
\begin{align*}
d(G \circ F)_p = d(\operatorname{id}_M)_p = \operatorname{id}_{T_pM}.
\end{align*}
Therefore
\begin{align*}
dG_q \circ dF_p = \operatorname{id}_{T_pM}.
\end{align*}
Applying the chain rule for differentials to $F \circ G: N \to N$ at $q$ gives
\begin{align*}
d(F \circ G)_q = dF_{G(q)} \circ dG_q.
\end{align*}
Since $G(q) = p$ and $F \circ G = \operatorname{id}_N$, we obtain
\begin{align*}
dF_p \circ dG_q = \operatorname{id}_{T_qN}.
\end{align*}
[guided]
We now turn the statement that $F$ and $G$ are inverse maps into a statement about their differentials. The two inverse identities are 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*}
The chain rule for differentials applies because $F$ and $G$ are smooth maps between smooth manifolds. Applying it to the composition $G \circ F: M \to M$ at the point $p$ gives
\begin{align*}
d(G \circ F)_p = dG_{F(p)} \circ dF_p.
\end{align*}
But $G \circ F$ is exactly the identity map on $M$. The differential of the identity map at $p$ is the identity linear map on $T_pM$, so
\begin{align*}
d(G \circ F)_p = d(\operatorname{id}_M)_p = \operatorname{id}_{T_pM}.
\end{align*}
Combining the two displayed identities gives
\begin{align*}
dG_{F(p)} \circ dF_p = \operatorname{id}_{T_pM}.
\end{align*}
Since $q$ was defined by $q := F(p)$, this is
\begin{align*}
dG_q \circ dF_p = \operatorname{id}_{T_pM}.
\end{align*}
We also need the reverse composition, because a two-sided inverse is what proves that a linear map is an isomorphism. Apply the chain rule to the composition $F \circ G: N \to N$ at the point $q \in N$. This gives
\begin{align*}
d(F \circ G)_q = dF_{G(q)} \circ dG_q.
\end{align*}
Since $G(q) = p$ and $F \circ G = \operatorname{id}_N$, the left-hand side is the identity linear map on $T_qN$. Hence
\begin{align*}
dF_p \circ dG_q = \operatorname{id}_{T_qN}.
\end{align*}
Thus $dG_q$ is simultaneously a left inverse and a right inverse for $dF_p$.
[/guided]
[/step]
[step:Conclude that the differential is a linear isomorphism]
We have shown that the linear maps
\begin{align*}
dF_p: T_pM \to T_qN
\end{align*}
and
\begin{align*}
dG_q: T_qN \to T_pM
\end{align*}
satisfy
\begin{align*}
dG_q \circ dF_p = \operatorname{id}_{T_pM}
\end{align*}
and
\begin{align*}
dF_p \circ dG_q = \operatorname{id}_{T_qN}.
\end{align*}
Therefore $dG_q$ is the inverse linear map of $dF_p$. Hence $dF_p$ is a linear isomorphism from $T_pM$ to $T_{F(p)}N$. Since $p \in M$ was arbitrary, the result holds for every $p \in M$.
[/step]
