[proofplan]
The statement is local, so we compare both sides in coordinate charts around $x \in M$ and $F(x) \in N$. In such charts, the diffeomorphism $F$ is represented by a Euclidean diffeomorphism $f$, and the local representative of the pullback distribution $F^*u$ is exactly the Euclidean pullback $f^*u_\psi$. The Euclidean wave front transformation law then gives the corresponding coordinate-level equality, and the chart transformation rule for cotangent vectors identifies the Euclidean transpose Jacobian with the intrinsic cotangent pullback $dF_x^\top$.
[/proofplan]
[step:Localize the statement in compatible coordinate charts]
Fix $x_0 \in M$ and set $y_0 := F(x_0) \in N$. Choose a coordinate chart $(U,\varphi)$ on $M$ with $x_0 \in U$ and a coordinate chart $(V,\psi)$ on $N$ with $y_0 \in V$. Replacing $U$ by $U \cap F^{-1}(V)$, we may assume $F(U) \subset V$.
Define the coordinate domains $\Omega := \varphi(U) \subset \mathbb{R}^m$ and $\Omega' := \psi(V) \subset \mathbb{R}^m$, where $m = \dim M = \dim N$. Define the coordinate representative of $F$ by
\begin{align*}
f: \Omega \to \Omega', \quad f(a)=\psi(F(\varphi^{-1}(a))).
\end{align*}
Because $F$, $\varphi$, and $\psi$ are diffeomorphisms onto their images, $f$ is a diffeomorphism between open subsets of $\mathbb{R}^m$.
Let $u_\psi \in \mathcal{D}'(\Omega')$ denote the local coordinate representative of $u|_V$, defined by pulling $u|_V$ through the chart $\psi^{-1}: \Omega' \to V$ according to the distributional chart convention. Let $(F^*u)_\varphi \in \mathcal{D}'(\Omega)$ denote the local coordinate representative of $(F^*u)|_U$ through $\varphi^{-1}: \Omega \to U$. By the definition of the distributional pullback by a diffeomorphism and by compatibility of pullback with composition,
\begin{align*}
(F^*u)_\varphi = f^*u_\psi
\end{align*}
as distributions on $\Omega$.
[/step]
[step:Translate manifold wave front membership into coordinate wave front membership]
Let $\xi_0 \in T_{x_0}^*M \setminus \{0\}$. Define the coordinate covector $\zeta_0 \in T_{\varphi(x_0)}^*\Omega \setminus \{0\}$ by
\begin{align*}
\zeta_0 := (d\varphi_{x_0}^{-1})^\top \xi_0.
\end{align*}
By the definition of the wave front set on a smooth manifold in local coordinates,
\begin{align*}
(x_0,\xi_0)\in \operatorname{WF}(F^*u)
\end{align*}
if and only if
\begin{align*}
(\varphi(x_0),\zeta_0)\in \operatorname{WF}((F^*u)_\varphi).
\end{align*}
Using $(F^*u)_\varphi=f^*u_\psi$, this is equivalent to
\begin{align*}
(\varphi(x_0),\zeta_0)\in \operatorname{WF}(f^*u_\psi).
\end{align*}
[guided]
We now reduce the intrinsic statement to the Euclidean statement. The point $x_0 \in M$ has coordinate representative $\varphi(x_0)\in \Omega$. A covector $\xi_0 \in T_{x_0}^*M$ must also be transported into coordinates. The correct coordinate covector is
\begin{align*}
\zeta_0 := (d\varphi_{x_0}^{-1})^\top \xi_0.
\end{align*}
This means that $\zeta_0$ acts on a coordinate tangent vector $v \in T_{\varphi(x_0)}\Omega$ by first sending $v$ back to $T_{x_0}M$ using $d\varphi_{x_0}^{-1}$ and then applying $\xi_0$.
By the definition of the wave front set on a smooth manifold, membership in $\operatorname{WF}(F^*u)$ is tested in any coordinate chart by this transported covector. Therefore
\begin{align*}
(x_0,\xi_0)\in \operatorname{WF}(F^*u)
\end{align*}
holds exactly when
\begin{align*}
(\varphi(x_0),\zeta_0)\in \operatorname{WF}((F^*u)_\varphi).
\end{align*}
By the definition of the distributional pullback in charts, the local coordinate representative $(F^*u)_\varphi \in \mathcal{D}'(\Omega)$ is the Euclidean pullback of the local coordinate representative $u_\psi \in \mathcal{D}'(\Omega')$ through the coordinate diffeomorphism $f: \Omega \to \Omega'$. Thus
\begin{align*}
(F^*u)_\varphi = f^*u_\psi.
\end{align*}
Substituting this equality of distributions, the preceding wave front membership condition is the same as
\begin{align*}
(\varphi(x_0),\zeta_0)\in \operatorname{WF}(f^*u_\psi).
\end{align*}
This is the point where the manifold problem has become a Euclidean microlocal problem.
[/guided]
[/step]
[step:Apply the Euclidean diffeomorphism transformation law]
We use the Euclidean wave front transformation theorem for diffeomorphisms: if $f:\Omega\to\Omega'$ is a diffeomorphism between open subsets of $\mathbb{R}^m$ and $v\in\mathcal{D}'(\Omega')$, then
\begin{align*}
\operatorname{WF}(f^*v)=\{(a,df_a^\top\theta):(f(a),\theta)\in\operatorname{WF}(v)\}.
\end{align*}
This is the Euclidean wave front transformation law for diffeomorphisms, used here as the local prerequisite; no internal theorem link is inserted here because no verified theorem identifier is available in the present specification.
Applying this theorem to $v=u_\psi$ and $a_0:=\varphi(x_0)$ gives
\begin{align*}
(\varphi(x_0),\zeta_0)\in \operatorname{WF}(f^*u_\psi)
\end{align*}
if and only if there exists $\theta_0\in T_{\psi(y_0)}^*\Omega'\setminus\{0\}$ such that
\begin{align*}
(\psi(y_0),\theta_0)\in\operatorname{WF}(u_\psi)
\end{align*}
and
\begin{align*}
\zeta_0=df_{\varphi(x_0)}^\top\theta_0.
\end{align*}
[guided]
We now apply the Euclidean theorem to the coordinate representative. The theorem requires three pieces of input: open subsets $\Omega,\Omega'\subset\mathbb{R}^m$, a diffeomorphism $f:\Omega\to\Omega'$, and a distribution $v\in\mathcal{D}'(\Omega')$. These hypotheses hold because $\Omega=\varphi(U)$ and $\Omega'=\psi(V)$ are coordinate domains, $f=\psi\circ F\circ\varphi^{-1}$ is a diffeomorphism between them, and $u_\psi\in\mathcal{D}'(\Omega')$ is the local coordinate representative of $u$.
The Euclidean wave front transformation law for diffeomorphisms gives
\begin{align*}
\operatorname{WF}(f^*u_\psi)=\{(a,df_a^\top\theta):(f(a),\theta)\in\operatorname{WF}(u_\psi)\}.
\end{align*}
Taking $a_0:=\varphi(x_0)$ and using $f(a_0)=\psi(F(x_0))=\psi(y_0)$, we obtain that
\begin{align*}
(\varphi(x_0),\zeta_0)\in \operatorname{WF}(f^*u_\psi)
\end{align*}
holds if and only if there exists a nonzero covector $\theta_0\in T_{\psi(y_0)}^*\Omega'$ such that
\begin{align*}
(\psi(y_0),\theta_0)\in\operatorname{WF}(u_\psi)
\end{align*}
and
\begin{align*}
\zeta_0=df_{\varphi(x_0)}^\top\theta_0.
\end{align*}
[/guided]
[/step]
[step:Identify the coordinate transpose with the intrinsic cotangent pullback]
Define the intrinsic covector $\eta_0\in T_{y_0}^*N$ corresponding to $\theta_0$ by
\begin{align*}
\eta_0 := d\psi_{y_0}^\top\theta_0.
\end{align*}
Equivalently, $\theta_0=(d\psi_{y_0}^{-1})^\top\eta_0$. By the manifold definition of wave front set,
\begin{align*}
(\psi(y_0),\theta_0)\in\operatorname{WF}(u_\psi)
\end{align*}
if and only if
\begin{align*}
(y_0,\eta_0)\in\operatorname{WF}(u).
\end{align*}
It remains to identify the covector transformation. Since
\begin{align*}
f=\psi\circ F\circ\varphi^{-1},
\end{align*}
the chain rule gives
\begin{align*}
df_{\varphi(x_0)}=d\psi_{y_0}\circ dF_{x_0}\circ d\varphi_{x_0}^{-1}.
\end{align*}
Taking cotangent pullbacks reverses the order of composition, so
\begin{align*}
df_{\varphi(x_0)}^\top\theta_0=(d\varphi_{x_0}^{-1})^\top dF_{x_0}^\top d\psi_{y_0}^\top\theta_0.
\end{align*}
Using $\eta_0=d\psi_{y_0}^\top\theta_0$, this becomes
\begin{align*}
df_{\varphi(x_0)}^\top\theta_0=(d\varphi_{x_0}^{-1})^\top dF_{x_0}^\top\eta_0.
\end{align*}
Since $\zeta_0=(d\varphi_{x_0}^{-1})^\top\xi_0$, the equality $\zeta_0=df_{\varphi(x_0)}^\top\theta_0$ is therefore equivalent to
\begin{align*}
\xi_0=dF_{x_0}^\top\eta_0.
\end{align*}
[guided]
The covector $\theta_0$ is still a coordinate covector on $\Omega'$. To return to the manifold $N$, define
\begin{align*}
\eta_0 := d\psi_{y_0}^\top\theta_0\in T_{y_0}^*N.
\end{align*}
Equivalently, $\theta_0=(d\psi_{y_0}^{-1})^\top\eta_0$. By the definition of the wave front set on a smooth manifold in local coordinates,
\begin{align*}
(\psi(y_0),\theta_0)\in\operatorname{WF}(u_\psi)
\end{align*}
is equivalent to
\begin{align*}
(y_0,\eta_0)\in\operatorname{WF}(u).
\end{align*}
It remains to check that the Euclidean transpose Jacobian is exactly the coordinate form of the intrinsic cotangent pullback. Since
\begin{align*}
f=\psi\circ F\circ\varphi^{-1},
\end{align*}
the chain rule gives
\begin{align*}
df_{\varphi(x_0)}=d\psi_{y_0}\circ dF_{x_0}\circ d\varphi_{x_0}^{-1}.
\end{align*}
Cotangent pullback reverses composition, so
\begin{align*}
df_{\varphi(x_0)}^\top\theta_0=(d\varphi_{x_0}^{-1})^\top dF_{x_0}^\top d\psi_{y_0}^\top\theta_0.
\end{align*}
Using $\eta_0=d\psi_{y_0}^\top\theta_0$, this becomes
\begin{align*}
df_{\varphi(x_0)}^\top\theta_0=(d\varphi_{x_0}^{-1})^\top dF_{x_0}^\top\eta_0.
\end{align*}
The coordinate covector attached to $\xi_0$ was defined by $\zeta_0=(d\varphi_{x_0}^{-1})^\top\xi_0$. Therefore the coordinate equality $\zeta_0=df_{\varphi(x_0)}^\top\theta_0$ is equivalent, after applying the inverse of the linear isomorphism $(d\varphi_{x_0}^{-1})^\top$, to
\begin{align*}
\xi_0=dF_{x_0}^\top\eta_0.
\end{align*}
[/guided]
[/step]
[step:Patch the local equivalence into the global equality]
Combining the previous steps, for every $x_0\in M$ and every nonzero $\xi_0\in T_{x_0}^*M$,
\begin{align*}
(x_0,\xi_0)\in\operatorname{WF}(F^*u)
\end{align*}
if and only if there exists $\eta_0\in T_{F(x_0)}^*N\setminus\{0\}$ such that
\begin{align*}
(F(x_0),\eta_0)\in\operatorname{WF}(u)
\end{align*}
and
\begin{align*}
\xi_0=dF_{x_0}^\top\eta_0.
\end{align*}
Because $dF_{x_0}:T_{x_0}M\to T_{F(x_0)}N$ is a linear isomorphism, its cotangent pullback $dF_{x_0}^\top:T_{F(x_0)}^*N\to T_{x_0}^*M$ is also a linear isomorphism and sends nonzero covectors to nonzero covectors. Therefore the preceding equivalence is exactly
\begin{align*}
\operatorname{WF}(F^*u)=\{(x,dF_x^\top\eta)\in \dot T^*M:(F(x),\eta)\in \operatorname{WF}(u)\}.
\end{align*}
This proves the theorem.
[/step]
