[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*}[/step]

[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: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]