[proofplan] We prove equality by checking membership at each nonzero covector $p \in T^*X \setminus 0$. If $p$ is outside the right-hand intersection, then some properly supported order-zero operator is elliptic at $p$ and sends $u$ to a smooth function, so elliptic regularity removes $p$ from $\operatorname{WF}(u)$. Conversely, if $p \notin \operatorname{WF}(u)$, the elliptic cutoff criterion for wave front sets gives an order-zero microlocal cutoff elliptic at $p$ whose application to $u$ is smooth; after inserting a proper-support kernel cutoff equal to $1$ near the relevant diagonal, the same microlocal conclusion remains valid. These two implications are precisely the stated intersection formula. [/proofplan]

[step:Define the comparison set and reduce the theorem to two pointwise implications] Define the set \begin{align*} E := \bigcap \left\{ \operatorname{Char}(A) : A \in \Psi^0_{\mathrm{prop}}(X) \text{ and } Au \in C^\infty(X) \right\} \subset T^*X \setminus 0. \end{align*} We prove $\operatorname{WF}(u)=E$ by proving both inclusions. Since both $\operatorname{WF}(u)$ and every $\operatorname{Char}(A)$ are conic subsets of $T^*X \setminus 0$, it is enough to argue at an arbitrary covector \begin{align*} p=(x_0,\xi_0) \in T^*X \setminus 0. \end{align*} The desired equality is equivalent to the following two statements: If $p \notin E$, then $p \notin \operatorname{WF}(u)$. If $p \notin \operatorname{WF}(u)$, then $p \notin E$. [/step]

[step:Use an elliptic smoothing operator to show $E \subset \operatorname{WF}(u)$] Assume $p \notin E$. By the definition of $E$, there exists an operator \begin{align*} A \in \Psi^0_{\mathrm{prop}}(X) \end{align*} such that $Au \in C^\infty(X)$ and $p \notin \operatorname{Char}(A)$. Since $\operatorname{Char}(A)$ is the complement of $\operatorname{Ell}(A)$ in $T^*X \setminus 0$, this means \begin{align*} p \in \operatorname{Ell}(A). \end{align*} By elliptic microlocal regularity for properly supported pseudodifferential operators, applied to the order-zero operator $A$ which is elliptic at $p$ and satisfies $Au \in C^\infty(X)$, we obtain \begin{align*} p \notin \operatorname{WF}(u). \end{align*} Thus $p \notin E$ implies $p \notin \operatorname{WF}(u)$, and hence \begin{align*} \operatorname{WF}(u) \subset E. \end{align*} Here the invoked prerequisite is the standard elliptic microlocal regularity statement: if $A$ is elliptic at $p$ and $Au$ is smooth near the base point of $p$, then $u$ is microlocally smooth at $p$. [/step]

[step:Construct a properly supported elliptic cutoff when $p \notin \operatorname{WF}(u)$]Assume now that \begin{align*} p=(x_0,\xi_0) \notin \operatorname{WF}(u). \end{align*} By the [elliptic cutoff criterion for the wave front set](/theorems/8173), there exists an order-zero pseudodifferential operator \begin{align*} B:C_c^\infty(X) \to C^\infty(X) \end{align*} whose full symbol is elliptic in a conic neighbourhood of $p$ and such that $Bu \in C^\infty(X)$ microlocally near $p$. We now arrange proper support without changing the operator microlocally at $p$. Choose an open coordinate neighbourhood $U_0 \subset X$ of $x_0$ and a conic neighbourhood $\Gamma_0 \subset T^*U_0 \setminus 0$ of $p$ on which $B$ is elliptic and on which $Bu$ is smooth. Choose a smooth cutoff \begin{align*} \rho:X \times X \to [0,1] \end{align*} such that $\rho$ is properly supported as a kernel cutoff and $\rho=1$ on a neighbourhood of the diagonal over a smaller neighbourhood $U_1 \Subset U_0$ of $x_0$. Let $K_B \in \mathcal{D}'(X \times X)$ denote the Schwartz kernel of $B$, and define the operator \begin{align*} A:C_c^\infty(X) &\to C^\infty(X) \end{align*} to be the pseudodifferential operator whose Schwartz kernel is \begin{align*} K_A := \rho K_B. \end{align*} Because $\rho$ is properly supported as a kernel cutoff, $K_A$ is properly supported. Hence \begin{align*} A \in \Psi^0_{\mathrm{prop}}(X). \end{align*} Since $\rho=1$ near the diagonal over $U_1$, the kernels $K_A$ and $K_B$ agree in a neighbourhood of the diagonal over $U_1$. Therefore $A-B$ is smoothing microlocally over $U_1$, and the principal symbols of $A$ and $B$ agree on a possibly smaller conic neighbourhood $\Gamma_1 \subset \Gamma_0$ of $p$. In particular, \begin{align*} p \in \operatorname{Ell}(A). \end{align*} It remains to record smoothness of $Au$. Let $\operatorname{WF}'(A) \subset T^*X \setminus 0$ denote the operator wave front set, equivalently the essential support of the full symbol of $A$ away from the zero section. Because $\operatorname{WF}(u)$ is closed and conic in $T^*X \setminus 0$ and $p \notin \operatorname{WF}(u)$, choose a conic open neighbourhood $\Gamma_2 \subset T^*X \setminus 0$ of $p$ such that $\Gamma_2 \cap \operatorname{WF}(u)=\varnothing$. Choose the preceding properly supported order-zero cutoff $A$ with $p \in \operatorname{Ell}(A)$ and $\operatorname{WF}'(A) \subset \Gamma_2$. The microlocal mapping property of pseudodifferential operators gives \begin{align*} \operatorname{WF}(Au) \subset \operatorname{WF}'(A) \cap \operatorname{WF}(u)=\varnothing. \end{align*} Since a distribution has empty wave front set exactly when it is smooth, this gives \begin{align*} Au \in C^\infty(X). \end{align*} Thus there exists $A \in \Psi^0_{\mathrm{prop}}(X)$ such that $Au \in C^\infty(X)$ and $p \in \operatorname{Ell}(A)$.[/step]

[guided]We start from the microlocal assumption $p \notin \operatorname{WF}(u)$. The meaning of this assumption is that $u$ has no singularity at the covector $p=(x_0,\xi_0)$. The elliptic cutoff criterion for the wave front set converts this absence of singularity into an operator statement: there is an order-zero pseudodifferential cutoff $B$ which is elliptic at $p$ and which kills all singularities of $u$ in a conic neighbourhood of $p$. The remaining point is support. The theorem only allows properly supported operators, because proper support guarantees that the operator acts continuously on distributions. So we choose an open coordinate neighbourhood $U_0 \subset X$ of $x_0$ and a conic neighbourhood $\Gamma_0 \subset T^*U_0 \setminus 0$ of $p$ where the operator $B$ is elliptic and where $Bu$ is smooth. Then we choose a smooth function \begin{align*} \rho:X \times X \to [0,1] \end{align*} which is properly supported as a kernel cutoff and which equals $1$ near the diagonal over a smaller neighbourhood $U_1 \Subset U_0$ of $x_0$. Let $K_B \in \mathcal{D}'(X \times X)$ be the Schwartz kernel of $B$. We define a new operator $A$ by declaring its Schwartz kernel to be \begin{align*} K_A := \rho K_B. \end{align*} Because the support of $\rho$ is proper over both factors of $X \times X$, the kernel $K_A$ is properly supported. Therefore \begin{align*} A \in \Psi^0_{\mathrm{prop}}(X). \end{align*} Why does this modification preserve ellipticity at $p$? Pseudodifferential symbols are determined microlocally by the kernel near the diagonal. Since $\rho=1$ near the diagonal over $U_1$, the kernels $K_A$ and $K_B$ agree there. Hence the difference $A-B$ is smoothing microlocally over $U_1$, and $A$ and $B$ have the same principal symbol on a smaller conic neighbourhood $\Gamma_1 \subset \Gamma_0$ of $p$. Since $B$ was elliptic on $\Gamma_0$, the operator $A$ is elliptic at $p$: \begin{align*} p \in \operatorname{Ell}(A). \end{align*} Finally, we need the global condition $Au \in C^\infty(X)$, not merely microlocal smoothness near $p$. Let $\operatorname{WF}'(A) \subset T^*X \setminus 0$ denote the operator wave front set, equivalently the essential support of the full symbol of $A$ away from the zero section. Since $\operatorname{WF}(u)$ is closed and conic and $p \notin \operatorname{WF}(u)$, we can choose a conic open neighbourhood $\Gamma_2 \subset T^*X \setminus 0$ of $p$ such that $\Gamma_2 \cap \operatorname{WF}(u)=\varnothing$. The properly supported symbol construction lets us choose the cutoff $A$ elliptic at $p$ with $\operatorname{WF}'(A) \subset \Gamma_2$. For such a choice, the microlocal mapping property of pseudodifferential operators gives \begin{align*} \operatorname{WF}(Au) \subset \operatorname{WF}'(A) \cap \operatorname{WF}(u)=\varnothing. \end{align*} A distribution has empty wave front set exactly when it is smooth, so \begin{align*} Au \in C^\infty(X). \end{align*} Thus we have constructed an operator $A \in \Psi^0_{\mathrm{prop}}(X)$ satisfying both required properties: it is elliptic at $p$, and it sends $u$ to a smooth function.[/guided]

[step:Use the constructed cutoff to show $\operatorname{WF}(u) \subset E$ has the reverse implication] From the previous step, if $p \notin \operatorname{WF}(u)$, then there exists \begin{align*} A \in \Psi^0_{\mathrm{prop}}(X) \end{align*} such that $Au \in C^\infty(X)$ and $p \in \operatorname{Ell}(A)$. Since \begin{align*} \operatorname{Char}(A)=(T^*X \setminus 0)\setminus \operatorname{Ell}(A), \end{align*} we have \begin{align*} p \notin \operatorname{Char}(A). \end{align*} This operator $A$ belongs to the family indexing the intersection defining $E$, but $p$ is not in its characteristic set. Therefore \begin{align*} p \notin E. \end{align*} Thus $p \notin \operatorname{WF}(u)$ implies $p \notin E$, which is equivalent to \begin{align*} E \subset \operatorname{WF}(u). \end{align*} [/step]

[step:Combine the two inclusions to obtain the intersection formula] We have proved \begin{align*} \operatorname{WF}(u) \subset E \end{align*} and \begin{align*} E \subset \operatorname{WF}(u). \end{align*} Therefore \begin{align*} \operatorname{WF}(u)=E. \end{align*} Substituting the definition of $E$ gives \begin{align*} \operatorname{WF}(u) = \bigcap \left\{ \operatorname{Char}(A) : A \in \Psi^0_{\mathrm{prop}}(X) \text{ and } Au \in C^\infty(X) \right\}. \end{align*} This is the claimed pseudodifferential characterization of the wave front set. [/step]