[proofplan] We prove the contrapositive local statement at a fixed covector $\rho_0 = (x_0,\xi_0)$. Since $\rho_0$ is not characteristic, $P$ is elliptic in a conic neighbourhood of $\rho_0$, so we choose a pseudodifferential cutoff $A$ elliptic at $\rho_0$ and supported microlocally inside that elliptic region. The microlocal elliptic parametrix gives an identity $A = QP + R$ near $\rho_0$, with $Q$ pseudodifferential and $R$ smoothing. If $Pu$ is microlocally smooth at $\rho_0$, then the term $QPu$ is smooth microlocally there, while $Ru$ is smooth because $R$ is smoothing; hence $Au$ is smooth, which is exactly the pseudodifferential criterion for $\rho_0 \notin WF(u)$. [/proofplan]

[step:Localize to a conic region where $P$ is elliptic]Fix $\rho_0 = (x_0,\xi_0) \in T^*X \setminus 0$ such that $\rho_0 \notin \operatorname{Char}(P)$ and $\rho_0 \notin WF(Pu)$. By the definition of the characteristic set, there exists an open conic neighbourhood $\Gamma \subset T^*X \setminus 0$ of $\rho_0$ on which $P$ is elliptic. Choose an operator \begin{align*} A: \mathcal{D}'(X) \to \mathcal{D}'(X) \end{align*} with $A \in \Psi^0(X)$, properly supported, elliptic at $\rho_0$, and with operator wave front set $WF'(A)$ contained in $\Gamma$ after shrinking $\Gamma$ if necessary. Here $WF'(A)$ denotes the microlocal support of the Schwartz kernel of $A$ as an operator on distributions. Because $\rho_0 \notin WF(Pu)$, after shrinking $\Gamma$ again we may assume that $Pu$ is microlocally smooth on $\Gamma$: every properly supported pseudodifferential cutoff with operator wave front set contained in $\Gamma$ sends $Pu$ to a smooth function.[/step]

[guided]We fix the covector \begin{align*} \rho_0 = (x_0,\xi_0) \in T^*X \setminus 0 \end{align*} and assume both $\rho_0 \notin \operatorname{Char}(P)$ and $\rho_0 \notin WF(Pu)$. The goal is to prove $\rho_0 \notin WF(u)$. The condition $\rho_0 \notin \operatorname{Char}(P)$ means precisely that the principal symbol of $P$ is elliptic at $\rho_0$. Ellipticity is an open conic condition in $T^*X \setminus 0$, so there is an open conic neighbourhood $\Gamma \subset T^*X \setminus 0$ of $\rho_0$ such that $P$ is elliptic throughout $\Gamma$. We now choose a microlocal cutoff \begin{align*} A: \mathcal{D}'(X) \to \mathcal{D}'(X) \end{align*} with $A \in \Psi^0(X)$, properly supported, elliptic at $\rho_0$, and $WF'(A) \subset \Gamma$. The point of choosing $A$ is that the wave front set criterion says that $\rho_0 \notin WF(u)$ once some order-zero pseudodifferential operator elliptic at $\rho_0$ sends $u$ to a smooth function. Thus the rest of the proof is devoted to proving $Au \in C^\infty(X)$. The condition $\rho_0 \notin WF(Pu)$ says that $Pu$ is microlocally smooth at $\rho_0$. By shrinking the conic neighbourhood $\Gamma$ around $\rho_0$, we may arrange that this smoothness holds throughout $\Gamma$: any properly supported pseudodifferential operator whose operator wave front set is contained in $\Gamma$ sends $Pu$ to a smooth function. This is the microlocal form of the defining cutoff criterion for the wave front set.[/guided]

[step:Construct a microlocal parametrix for $P$ on the support of $A$]We use the standard microlocal elliptic parametrix theorem (citing a result not yet in the wiki: microlocal elliptic parametrix construction). Since $P$ is elliptic on the conic neighbourhood $\Gamma$ and $WF'(A) \subset \Gamma$, there are a smaller open conic neighbourhood $\Gamma_0 \subset \Gamma$ of $\rho_0$ and properly supported operators \begin{align*} Q: \mathcal{D}'(X) \to \mathcal{D}'(X) \end{align*} with $Q \in \Psi^{-m}(X)$ and $WF'(Q) \subset \Gamma$, and \begin{align*} R: \mathcal{D}'(X) \to C^\infty(X) \end{align*} with $R \in \Psi^{-\infty}(X)$, such that the residual operator $A - QP - R$ has operator wave front set disjoint from $\Gamma_0$. After replacing $A$ by a smaller cutoff elliptic at $\rho_0$ with $WF'(A) \subset \Gamma_0$ and absorbing this harmless residual into $R$, we may write \begin{align*} Au = Q(Pu) + Ru \end{align*} in $\mathcal{D}'(X)$.[/step]

[guided]The purpose of the parametrix is to invert $P$ only where ellipticity is available. The standard microlocal elliptic parametrix theorem applies because $P \in \Psi^m(X)$ is properly supported and elliptic on the open conic neighbourhood $\Gamma$, while the cutoff $A \in \Psi^0(X)$ has $WF'(A) \subset \Gamma$. The theorem gives a properly supported operator \begin{align*} Q: \mathcal{D}'(X) \to \mathcal{D}'(X) \end{align*} with $Q \in \Psi^{-m}(X)$ and $WF'(Q) \subset \Gamma$, so $Q$ is microlocally supported only where $P$ is elliptic. It also gives a smoothing operator \begin{align*} R: \mathcal{D}'(X) \to C^\infty(X) \end{align*} with $R \in \Psi^{-\infty}(X)$, where $\Psi^{-\infty}(X)$ is the class of operators with smooth Schwartz kernel mapping distributions to smooth functions. The precise microlocal identity is not just the formal equation $A = QP + R$ everywhere. What the construction gives is that, after choosing a smaller conic neighbourhood $\Gamma_0 \subset \Gamma$ of $\rho_0$, the residual operator $A - QP - R$ has operator wave front set disjoint from $\Gamma_0$. This means the residual cannot create a singularity at $\rho_0$. Replacing $A$ by a smaller cutoff still elliptic at $\rho_0$ and supported in $\Gamma_0$, we absorb the residual into the smoothing remainder. Therefore, when the identity is applied to the distribution $u \in \mathcal{D}'(X)$, it gives \begin{align*} Au = Q(Pu) + Ru \end{align*} in $\mathcal{D}'(X)$.[/guided]

[step:Show that both terms in the parametrix identity are smooth] Recall that $C^\infty(X)$ denotes the space of smooth functions on $X$, and that $\Psi^{-\infty}(X)$ denotes the smoothing operators, equivalently properly supported operators with smooth Schwartz kernel mapping $\mathcal{D}'(X)$ into $C^\infty(X)$. The operator $Q$ is properly supported and pseudodifferential, with microlocal support contained in the elliptic neighbourhood $\Gamma$ after the preceding construction. Since $Pu$ is microlocally smooth on $\Gamma$, the standard microlocal pseudolocal smoothness property for pseudodifferential operators applies to $Q$ and gives \begin{align*} Q(Pu) \in C^\infty(X). \end{align*} Here we are using the standard prerequisite that pseudodifferential operators preserve microlocal smoothness on regions where their operator wave front set is supported (citing a result not yet in the wiki: pseudodifferential operators preserve smoothness microlocally). The remainder $R$ belongs to $\Psi^{-\infty}(X)$, so its Schwartz kernel is smooth. Therefore the standard smoothing-operator theorem gives \begin{align*} Ru \in C^\infty(X) \end{align*} for every $u \in \mathcal{D}'(X)$ (citing a result not yet in the wiki: smoothing operators map distributions to smooth functions). Combining the two smoothness conclusions with \begin{align*} Au = Q(Pu) + Ru \end{align*} gives \begin{align*} Au \in C^\infty(X). \end{align*} [/step]

[step:Apply the pseudodifferential cutoff criterion for the wave front set] The operator $A \in \Psi^0(X)$ is elliptic at $\rho_0$, and the previous step proves $Au \in C^\infty(X)$. By the pseudodifferential criterion for absence from the wave front set (citing a result not yet in the wiki: pseudodifferential criterion for absence from the wave front set), this implies \begin{align*} \rho_0 \notin WF(u). \end{align*} We have shown that every $\rho_0 \in T^*X \setminus 0$ satisfying $\rho_0 \notin \operatorname{Char}(P)$ and $\rho_0 \notin WF(Pu)$ also satisfies $\rho_0 \notin WF(u)$. This is the contrapositive of \begin{align*} WF(u) \setminus \operatorname{Char}(P) \subset WF(Pu), \end{align*} and the theorem follows. [/step]