[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)$.
[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]
[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]
