[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$.
[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]
[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]
