[proofplan]
We prove the inclusion by contraposition at a fixed nonzero covector $\rho \in T^*X \setminus 0$. If $\rho$ is neither characteristic for $P$ nor in $WF^{s-m}(Pu)$, then $P$ is elliptic near $\rho$ and $Pu$ has microlocal Sobolev regularity $H^{s-m}$ near $\rho$. A microlocal parametrix for $P$ converts this regularity into $H^s$ regularity for an elliptic cutoff of $u$, while the remainder is smoothing and hence harmless. Therefore $\rho \notin WF^s(u)$.
[/proofplan]
[step:Fix a covector outside the right-hand side and translate the wave front assumptions]
Let $\rho = (x_0,\xi_0) \in T^*X \setminus 0$ satisfy
\begin{align*}
\rho \notin WF^{s-m}(Pu) \cup \operatorname{Char}(P).
\end{align*}
We must prove $\rho \notin WF^s(u)$.
Since $\rho \notin WF^{s-m}(Pu)$, by the definition of the Sobolev wave front set there exists a properly supported microlocal cutoff
\begin{align*}
A \in \Psi_{\mathrm{prop}}^0(X)
\end{align*}
whose principal symbol is elliptic at $\rho$ and such that
\begin{align*}
A(Pu) \in H_{\mathrm{loc}}^{s-m}(X).
\end{align*}
Since $\rho \notin \operatorname{Char}(P)$, the principal symbol of $P$ is elliptic on some conic neighbourhood $\Gamma \subset T^*X \setminus 0$ of $\rho$.
[guided]
We argue at one fixed covector because the desired statement is an inclusion of conic subsets of $T^*X \setminus 0$. Let
\begin{align*}
\rho = (x_0,\xi_0) \in T^*X \setminus 0
\end{align*}
be a covector which does not belong to the right-hand side:
\begin{align*}
\rho \notin WF^{s-m}(Pu) \cup \operatorname{Char}(P).
\end{align*}
To prove the theorem, it is enough to show $\rho \notin WF^s(u)$.
The first exclusion, $\rho \notin WF^{s-m}(Pu)$, means precisely, by the definition of the Sobolev wave front set stated in the theorem, that there exists an operator
\begin{align*}
A \in \Psi_{\mathrm{prop}}^0(X)
\end{align*}
whose principal symbol is elliptic at $\rho$ and for which
\begin{align*}
A(Pu) \in H_{\mathrm{loc}}^{s-m}(X).
\end{align*}
The second exclusion, $\rho \notin \operatorname{Char}(P)$, says that the order-$m$ principal symbol of $P$ is elliptic at $\rho$. Since ellipticity is an open conic condition on $T^*X \setminus 0$, after shrinking there is a conic neighbourhood
\begin{align*}
\Gamma \subset T^*X \setminus 0
\end{align*}
of $\rho$ on which both the principal symbol of $A$ and the principal symbol of $P$ are elliptic. Therefore the composed operator
\begin{align*}
AP \in \Psi_{\mathrm{prop}}^m(X)
\end{align*}
is properly supported and elliptic on $\Gamma$: proper support is preserved by composition of properly supported pseudodifferential operators, and the principal symbol of $AP$ is the product of the principal symbols of $A$ and $P$.
The microlocal parametrix theorem for elliptic pseudodifferential operators applied to $AP$ on $\Gamma$ gives properly supported operators
\begin{align*}
Q \in \Psi_{\mathrm{prop}}^{-m}(X)
\end{align*}
and
\begin{align*}
B \in \Psi_{\mathrm{prop}}^0(X)
\end{align*}
with $B$ elliptic at $\rho$, together with a smoothing remainder
\begin{align*}
R \in \Psi^{-\infty}(X),
\end{align*}
such that the operator identity
\begin{align*}
B = QAP + R
\end{align*}
holds after the microlocal cutoffs have been chosen inside $\Gamma$. Applying this identity to $u \in \mathcal{D}'(X)$ gives
\begin{align*}
Bu = Q(A(Pu)) + Ru.
\end{align*}
Now $Q$ has order $-m$ and is properly supported, so the Sobolev mapping property for pseudodifferential operators gives a continuous map from $H_{\mathrm{loc}}^{s-m}(X)$ to $H_{\mathrm{loc}}^s(X)$. Since $A(Pu) \in H_{\mathrm{loc}}^{s-m}(X)$, we obtain
\begin{align*}
Q(A(Pu)) \in H_{\mathrm{loc}}^s(X).
\end{align*}
Also, $R \in \Psi^{-\infty}(X)$ is smoothing, so $Ru$ is smooth and hence belongs to $H_{\mathrm{loc}}^s(X)$. The identity for $Bu$ therefore implies
\begin{align*}
Bu \in H_{\mathrm{loc}}^s(X).
\end{align*}
Because $B$ is elliptic at $\rho$, the definition of $WF^s(u)$ gives $\rho \notin WF^s(u)$. Thus every covector outside $WF^{s-m}(Pu) \cup \operatorname{Char}(P)$ is outside $WF^s(u)$, which is exactly the desired inclusion by contraposition.
[/guided]
[/step]
[step:Choose a microlocal parametrix compatible with the Sobolev cutoff]
Shrink $\Gamma$ if necessary so that $A$ remains elliptic on $\Gamma$. Since $A \in \Psi_{\mathrm{prop}}^0(X)$ and $P \in \Psi_{\mathrm{prop}}^m(X)$ are properly supported, their composition satisfies
\begin{align*}
AP \in \Psi_{\mathrm{prop}}^m(X).
\end{align*}
On $\Gamma$, the principal symbol of $AP$ is the product of the principal symbol of $A$ and the principal symbol of $P$, so $AP$ is elliptic on $\Gamma$.
By the microlocal parametrix theorem for elliptic pseudodifferential operators applied to $AP$ on $\Gamma$ (citing a result not yet in the wiki: Microlocal parametrix for elliptic pseudodifferential operators), there exist properly supported operators
\begin{align*}
Q \in \Psi_{\mathrm{prop}}^{-m}(X)
\end{align*}
and
\begin{align*}
B \in \Psi_{\mathrm{prop}}^0(X)
\end{align*}
such that $B$ is elliptic at $\rho$ and
\begin{align*}
B = QAP + R,
\end{align*}
where
\begin{align*}
R \in \Psi^{-\infty}(X)
\end{align*}
is a smoothing operator. Applying this operator identity to $u \in \mathcal{D}'(X)$ gives
\begin{align*}
Bu = Q(A(Pu)) + Ru.
\end{align*}
[/step]
[step:Use the Sobolev mapping property to control the parametrix term]
The operator $Q$ has order $-m$ and is properly supported. By the Sobolev mapping property for pseudodifferential operators (citing a result not yet in the wiki: Sobolev mapping property for pseudodifferential operators), $Q$ maps $H_{\mathrm{loc}}^{s-m}(X)$ continuously into $H_{\mathrm{loc}}^s(X)$. Since $A(Pu) \in H_{\mathrm{loc}}^{s-m}(X)$, it follows that
\begin{align*}
Q(A(Pu)) \in H_{\mathrm{loc}}^s(X).
\end{align*}
[/step]
[step:Use smoothing of the remainder to control the error term]
The remainder satisfies $R \in \Psi^{-\infty}(X)$. By the smoothing regularity property for pseudodifferential remainders (citing a result not yet in the wiki: [Smoothing operators improve Sobolev regularity](/theorems/7697) microlocally), for every distribution $v \in \mathcal{D}'(X)$ the distribution $Rv$ is smooth. Applying this to $v = u$ gives
\begin{align*}
Ru \in H_{\mathrm{loc}}^s(X).
\end{align*}
[/step]
[step:Conclude that the fixed covector is not in the Sobolev wave front set]
Combining the two previous steps with
\begin{align*}
Bu = Q(A(Pu)) + Ru,
\end{align*}
we obtain
\begin{align*}
Bu \in H_{\mathrm{loc}}^s(X).
\end{align*}
The operator $B \in \Psi_{\mathrm{prop}}^0(X)$ is elliptic at $\rho$. Therefore, by the definition of the Sobolev wave front set, $\rho \notin WF^s(u)$. We have shown that every
\begin{align*}
\rho \notin WF^{s-m}(Pu) \cup \operatorname{Char}(P)
\end{align*}
also satisfies $\rho \notin WF^s(u)$. This is the contrapositive of
\begin{align*}
WF^s(u) \subset WF^{s-m}(Pu) \cup \operatorname{Char}(P),
\end{align*}
which proves the theorem.
[/step]
