[proofplan] The proof is the standard parametrix argument for elliptic pseudodifferential operators. Ellipticity at $(x_0,\xi_0)$ gives a microlocal inverse $B \in \Psi^{-m}(U)$ in a conic neighbourhood of that point, with the defect equal to a microlocally smoothing operator. If $Au$ is microlocally smooth, then applying $B$ preserves that microlocal smoothness; the smoothing remainder is also microlocally smooth. The parametrix identity then writes $u$ microlocally as a difference of two microlocally smooth distributions, proving that $(x_0,\xi_0)$ is not in $\operatorname{WF}(u)$. [/proofplan]

[step:Localize the operator so that all distributional actions are defined] First assume that $A$ is properly supported. Then the action \begin{align*} A:\mathcal{D}'(U) \to \mathcal{D}'(U) \end{align*} is defined, and the same is true for every properly supported pseudodifferential operator used below. If $A$ is not properly supported, choose cutoffs $\psi,\chi \in C_c^\infty(U)$ such that $\psi = 1$ on an open neighbourhood $V_\psi \subset U$ of $x_0$ and $\chi = 1$ on an open neighbourhood $V_\chi \subset V_\psi$ of $x_0$. Define the localized operator \begin{align*} A_{\mathrm{loc}}:\mathcal{D}'(U) &\to \mathcal{D}'(U), \quad A_{\mathrm{loc}}u := \chi A(\psi u). \end{align*} Its Schwartz kernel is compactly supported in both variables, so it is properly supported. Since $\psi$ and $\chi$ are identically $1$ near $x_0$, $A_{\mathrm{loc}}$ has the same full symbol as $A$ in a neighbourhood of $(x_0,\xi_0)$. Thus ellipticity at $(x_0,\xi_0)$ and microlocal smoothness statements at $(x_0,\xi_0)$ are unchanged by replacing $A$ with $A_{\mathrm{loc}}$. It is therefore enough to prove the properly supported case. [/step]

[step:Choose a conic neighbourhood where the elliptic parametrix applies]Because $A$ is elliptic at $(x_0,\xi_0)$, there exists an open conic neighbourhood $\Gamma \subset T^*U \setminus 0$ of $(x_0,\xi_0)$ on which the principal symbol of $A$ is invertible in the sense required by the pseudodifferential calculus. By the microlocal parametrix theorem for elliptic pseudodifferential operators, citing a result not yet in the wiki: microlocal parametrix for elliptic pseudodifferential operators, there exist a properly supported operator $B \in \Psi^{-m}(U)$, an open conic neighbourhood $\Gamma_1 \subset \Gamma$ of $(x_0,\xi_0)$, and an operator $R \in \Psi^{-\infty}(U)$ microlocally on $\Gamma_1$ such that \begin{align*} BA = I + R \end{align*} microlocally on $\Gamma_1$. Here $I:\mathcal{D}'(U)\to\mathcal{D}'(U)$ denotes the identity operator. The sign of $R$ is immaterial: replacing $R$ by $-R$ if the parametrix convention gives $BA=I-R$, the identity has the displayed form. The phrase “microlocally on $\Gamma_1$” means that, after applying any order-zero microlocal cutoff whose essential support is contained in $\Gamma_1$, the difference between $BA-I-R$ and the zero operator is smoothing.[/step]

[guided]The only place where ellipticity is used is in constructing an inverse modulo smoothing errors. Since $A$ is elliptic at $(x_0,\xi_0)$, its principal symbol does not vanish in a sufficiently small open conic neighbourhood $\Gamma$ of $(x_0,\xi_0)$. This is exactly the hypothesis needed for the standard elliptic parametrix theorem in the pseudodifferential calculus. Applying that theorem, citing a result not yet in the wiki: microlocal parametrix for elliptic pseudodifferential operators, gives a properly supported operator \begin{align*} B:\mathcal{D}'(U) \to \mathcal{D}'(U) \end{align*} with $B \in \Psi^{-m}(U)$, together with a smaller open conic neighbourhood $\Gamma_1 \subset \Gamma$ of $(x_0,\xi_0)$ and a remainder operator $R$ which is smoothing microlocally on $\Gamma_1$. The parametrix identity is \begin{align*} BA = I + R \end{align*} microlocally on $\Gamma_1$. This identity should not be read as a global equality of kernels on all of $U \times U$. It means that if we test the identity by a microlocal cutoff supported inside $\Gamma_1$, then the error is smoothing. That localized interpretation is exactly what is needed, because the theorem only asks about the single cotangent direction $(x_0,\xi_0)$.[/guided]

[step:Transfer microlocal smoothness from $Au$ to $BAu$] Assume \begin{align*} (x_0,\xi_0) \notin \operatorname{WF}(Au). \end{align*} Since $\Gamma_1$ is an open conic neighbourhood of $(x_0,\xi_0)$, shrink $\Gamma_1$ if necessary so that $Au$ is microlocally smooth throughout $\Gamma_1$. The operator $B$ is a pseudodifferential operator, and pseudodifferential operators do not create wave front set outside the wave front set of the input, citing a result not yet in the wiki: pseudodifferential operators preserve microlocal smoothness. Hence $BAu$ is microlocally smooth at $(x_0,\xi_0)$: \begin{align*} (x_0,\xi_0) \notin \operatorname{WF}(BAu). \end{align*} [/step]

[step:Use the smoothing remainder to remove the remaining singular term] The remainder $R$ is smoothing microlocally on $\Gamma_1$. Therefore, by the microlocally smoothing remainder property, citing a result not yet in the wiki: microlocally smoothing operators remove wave front set in their smoothing region, for every $u \in \mathcal{D}'(U)$ one has \begin{align*} \operatorname{WF}(Ru) \cap \Gamma_1 = \varnothing. \end{align*} In particular, \begin{align*} (x_0,\xi_0) \notin \operatorname{WF}(Ru). \end{align*} [/step]

[step:Rearrange the parametrix identity to recover microlocal smoothness of $u$] Applying the microlocal identity $BA=I+R$ to $u$ gives \begin{align*} BAu = u + Ru \end{align*} microlocally on $\Gamma_1$. Equivalently, \begin{align*} u = BAu - Ru \end{align*} microlocally on $\Gamma_1$. The distribution $BAu$ is microlocally smooth at $(x_0,\xi_0)$ by the preceding step, and $Ru$ is microlocally smooth at $(x_0,\xi_0)$ because $R$ is microlocally smoothing there. Since the wave front set is closed under addition in the sense that \begin{align*} \operatorname{WF}(v+w) \subset \operatorname{WF}(v) \cup \operatorname{WF}(w) \end{align*} for distributions $v,w \in \mathcal{D}'(U)$, citing a result not yet in the wiki: wave front set of a sum is contained in the union of wave front sets, the right-hand side $BAu-Ru$ is microlocally smooth at $(x_0,\xi_0)$. Thus \begin{align*} (x_0,\xi_0) \notin \operatorname{WF}(u). \end{align*} This proves the elliptic detection principle. [/step]