[proofplan] We prove the equivalent pointwise statement. Fix a nonzero covector $\rho_0 = (x_0,\xi_0)$ where $P$ is elliptic and where $Pu$ is microlocally smooth. We localize to a conic neighborhood of $\rho_0$, choose a microlocal parametrix $Q$ for $P$ there, and then apply an elliptic cutoff $B$ at $\rho_0$ to the identity $QP = I$ modulo microlocally smoothing errors. The resulting formula writes $Bu$ as a sum of smooth terms, so the elliptic cutoff characterization of the wave front set excludes $\rho_0$ from $WF(u)$. [/proofplan]

[step:Fix a covector outside the wave front set of $Pu$ and the characteristic set of $P$] Let \begin{align*} \rho_0 := (x_0,\xi_0) \in T^*X \setminus 0 \end{align*} be such that $\rho_0 \notin WF(Pu) \cup \operatorname{Char}(P)$. Since $\rho_0 \notin \operatorname{Char}(P)$, the operator $P$ is elliptic at $\rho_0$. Since $\rho_0 \notin WF(Pu)$, the elliptic cutoff characterization of the wave front set gives a properly supported operator $A \in \Psi^0_{\mathrm{prop}}(X)$, elliptic at $\rho_0$, such that \begin{align*} A(Pu) \in C^\infty(X). \end{align*} Here $A: \mathcal{D}'(X) \to \mathcal{D}'(X)$ denotes the continuous extension of the pseudodifferential operator to distributions. The proper support of $P$ ensures that $Pu \in \mathcal{D}'(X)$ is globally defined. [/step]

[step:Choose a conic region where $P$ is elliptic and $Pu$ is microlocally smooth]Choose an open conic neighborhood $\Gamma \subset T^*X \setminus 0$ of $\rho_0$ such that $P$ is elliptic on $\Gamma$ and $A$ is elliptic on $\Gamma$. This is possible because ellipticity is an open condition in the cotangent variables and because $A$ is elliptic at $\rho_0$. The condition $A(Pu) \in C^\infty(X)$ and ellipticity of $A$ on $\Gamma$ imply that $Pu$ is microlocally smooth on $\Gamma$. Equivalently, \begin{align*} WF(Pu) \cap \Gamma = \varnothing. \end{align*}[/step]

[guided]We need a single conic region where both ingredients are available: $P$ must be invertible microlocally, and $Pu$ must have no singularities. Let $\Gamma \subset T^*X \setminus 0$ be an open conic neighborhood of $\rho_0$ small enough that $P$ remains elliptic on $\Gamma$. Such a shrink is allowed because $\rho_0 \notin \operatorname{Char}(P)$ and ellipticity is stable under sufficiently small conic perturbations of the covector. We also shrink $\Gamma$ so that $A$ is elliptic on $\Gamma$. The operator $A \in \Psi^0_{\mathrm{prop}}(X)$ was chosen from the cutoff characterization of $\rho_0 \notin WF(Pu)$, and it satisfies $A(Pu) \in C^\infty(X)$. Since $A$ is elliptic on $\Gamma$, the same cutoff characterization says that $Pu$ has no wave front over $\Gamma$: \begin{align*} WF(Pu) \cap \Gamma = \varnothing. \end{align*} This step is where the two hypotheses on $\rho_0$ are separated. The condition $\rho_0 \notin \operatorname{Char}(P)$ supplies the region where a parametrix for $P$ exists. The condition $\rho_0 \notin WF(Pu)$ supplies the region where the right-hand side $Pu$ is already microlocally smooth.[/guided]

[step:Construct a microlocal parametrix for $P$ on the elliptic region] By the microlocal parametrix theorem for elliptic pseudodifferential operators (citing a result not yet in the wiki: Microlocal parametrix for elliptic pseudodifferential operators), applied to the operator $P \in \Psi^m_{\mathrm{prop}}(X)$ on the conic elliptic region $\Gamma$, there exists a properly supported operator \begin{align*} Q \in \Psi^{-m}_{\mathrm{prop}}(X) \end{align*} such that $QP$ equals the identity microlocally on $\Gamma$ modulo a microlocally smoothing error. More explicitly, after shrinking $\Gamma$ if necessary, we may choose an operator $R \in \Psi^{-\infty}_{\mathrm{prop}}(X)$ microlocally on $\Gamma$ such that \begin{align*} QP = I + R \end{align*} microlocally on $\Gamma$, where $I: \mathcal{D}'(X) \to \mathcal{D}'(X)$ is the identity operator. The phrase “microlocally on $\Gamma$” means that whenever a properly supported cutoff operator has operator wave front set contained in a sufficiently small conic subset of $\Gamma$, applying that cutoff to $QP - I - R$ gives a smoothing operator. [/step]

[step:Apply an elliptic cutoff and express $Bu$ by smooth terms] Choose $B \in \Psi^0_{\mathrm{prop}}(X)$ elliptic at $\rho_0$ whose operator wave front set is contained in $\Gamma$. By the microlocal identity from the previous step, define \begin{align*} S := B(QP - I - R). \end{align*} Then $S \in \Psi^{-\infty}_{\mathrm{prop}}(X)$ is smoothing. Applying the identity to $u \in \mathcal{D}'(X)$ gives \begin{align*} BQPu = Bu + BRu + Su. \end{align*} Rearranging, \begin{align*} Bu = BQ(Pu) - BRu - Su. \end{align*} The term $BQ(Pu)$ is smooth because $Pu$ is microlocally smooth on $\Gamma$, the operator wave front set of $BQ$ is contained in $\Gamma$, and pseudodifferential operators preserve microlocal smoothness (citing a result not yet in the wiki: Pseudodifferential operators preserve microlocal smoothness). The terms $BRu$ and $Su$ are smooth because $BR$ and $S$ are properly supported smoothing operators, and smoothing operators map distributions to smooth functions (citing a result not yet in the wiki: Smoothing operators remove wave front set). Hence \begin{align*} Bu \in C^\infty(X). \end{align*} [/step]

[step:Conclude that the original covector is not in $WF(u)$] The operator $B \in \Psi^0_{\mathrm{prop}}(X)$ is elliptic at $\rho_0$ and satisfies $Bu \in C^\infty(X)$. By the elliptic cutoff characterization of the wave front set, this implies \begin{align*} \rho_0 \notin WF(u). \end{align*} Since $\rho_0$ was an arbitrary element of $(T^*X \setminus 0) \setminus \bigl(WF(Pu) \cup \operatorname{Char}(P)\bigr)$, we have proved \begin{align*} WF(u) \subset WF(Pu) \cup \operatorname{Char}(P). \end{align*} This is the desired microlocal elliptic regularity inclusion. [/step]