[proofplan] The local diffeomorphism hypothesis already gives smoothness of $F$ locally, hence globally. Since $F$ is bijective, it has a set-theoretic inverse $G: N \to M$. Around each point $y \in N$, the map $G$ agrees with the smooth inverse of a local diffeomorphism branch of $F$, so $G$ is smooth locally. Therefore $F$ is a smooth bijection with smooth inverse, which is exactly a diffeomorphism. [/proofplan]

[step:Use the local diffeomorphism charts to prove that $F$ is smooth] Let $p \in M$. By hypothesis, there exist an open neighbourhood $U_p \subset M$ of $p$ and an open neighbourhood $V_p \subset N$ of $F(p)$ such that \begin{align*} F|_{U_p}: U_p \to V_p \end{align*} is a diffeomorphism. In particular, $F|_{U_p}$ is smooth. Since smoothness of a map between smooth manifolds is local on the domain and the sets $U_p$ cover $M$, the map \begin{align*} F: M \to N \end{align*} is smooth. [/step]

[step:Identify the global inverse with each local inverse branch]Since $F$ is bijective, define the inverse map \begin{align*} G: N \to M \end{align*} by declaring $G(y)$ to be the unique point $x \in M$ satisfying $F(x)=y$. Fix $y \in N$, and set $x := G(y)$. By the local diffeomorphism hypothesis at $x$, there exist open neighbourhoods $U_x \subset M$ of $x$ and $V_x \subset N$ of $F(x)=y$ such that $F(U_x)=V_x$ and \begin{align*} F|_{U_x}: U_x \to V_x \end{align*} is a diffeomorphism. Let \begin{align*} H_x: V_x \to U_x \end{align*} denote the inverse diffeomorphism of $F|_{U_x}$. We claim that $G|_{V_x}=H_x$. Indeed, if $z \in V_x$, then $H_x(z) \in U_x$ and \begin{align*} F(H_x(z)) = z. \end{align*} By the defining property of $G$, the point $G(z)$ is the unique element of $M$ mapped to $z$ by $F$. Hence $G(z)=H_x(z)$ for every $z \in V_x$.[/step]

[guided]The point of introducing the global inverse $G$ is that bijectivity makes it a well-defined map on all of $N$. Explicitly, for each $y \in N$, surjectivity gives at least one point $x \in M$ with $F(x)=y$, and injectivity makes that point unique. Thus the formula \begin{align*} G: N \to M \end{align*} with $G(y)$ equal to the unique solution of $F(x)=y$ defines a function. Now fix $y \in N$ and define $x := G(y)$. Since $F$ is a local diffeomorphism at this particular point $x$, there are open neighbourhoods $U_x \subset M$ of $x$ and $V_x \subset N$ of $F(x)=y$ such that \begin{align*} F|_{U_x}: U_x \to V_x \end{align*} is a diffeomorphism. Therefore this restricted map has a smooth inverse map \begin{align*} H_x: V_x \to U_x. \end{align*} We must check that this local inverse $H_x$ is not merely an inverse for the restricted map, but is exactly the restriction of the global inverse $G$ to $V_x$. Let $z \in V_x$. Since $H_x$ is the inverse of $F|_{U_x}$, the point $H_x(z) \in U_x$ satisfies \begin{align*} F(H_x(z)) = z. \end{align*} On the other hand, $G(z)$ is defined to be the unique point of $M$ whose image under $F$ is $z$. The uniqueness comes from injectivity of $F$. Therefore the two points must be equal: \begin{align*} G(z)=H_x(z). \end{align*} Since this holds for every $z \in V_x$, we have proved \begin{align*} G|_{V_x}=H_x. \end{align*} This is the key compatibility check: the locally defined inverse branches glue automatically because the global inverse is single-valued.[/guided]

[step:Conclude that the global inverse is smooth] Let $y \in N$. From the previous step, there is an open neighbourhood $V_x \subset N$ of $y$ and a smooth map \begin{align*} H_x: V_x \to U_x \subset M \end{align*} such that $G|_{V_x}=H_x$. Hence $G$ is smooth on an open neighbourhood of $y$. Since $y \in N$ was arbitrary and smoothness is local on the domain, the inverse map \begin{align*} G: N \to M \end{align*} is smooth. [/step]

[step:Assemble the definition of diffeomorphism] We have shown that $F: M \to N$ is smooth. By hypothesis, $F$ is bijective. Its inverse map $G=F^{-1}: N \to M$ is smooth by the preceding step. Therefore $F$ is a diffeomorphism from $M$ to $N$. [/step]