[proofplan]
We prove the estimate by constructing a microlocal inverse for $A$ on a small neighbourhood of $\operatorname{WF}_h(C)$. The ellipticity of $A$ gives a parametrix $B\in\Psi_h^{-m}(X)$ after inserting a zeroth-order cutoff $C_1$ which is elliptic on the microsupport of $C$. This gives a microlocal identity $C = C B C_1 A + R$, where $R$ is an $h^\infty$ smoothing remainder. The first term is controlled by the semiclassical Sobolev mapping estimate for pseudodifferential operators, while the smoothing remainder gives the rapidly decaying error $h^N\|u\|_{H_h^{-N}(X)}$.
[/proofplan]
[step:Choose a microlocal elliptic neighbourhood for the construction]
Let $a_m$ denote the scalar semiclassical principal symbol of $A$ near $(x_0,\xi_0)$. Since $A$ is semiclassically elliptic at $(x_0,\xi_0)$, there are an open neighbourhood $V_0\subset T^*X$ of $(x_0,\xi_0)$ and a local order $-m$ semiclassical symbol
\begin{align*}
b_{-m}:V_0\to\mathbb C
\end{align*}
such that
\begin{align*}
b_{-m}(x,\xi)a_m(x,\xi)=1
\end{align*}
for all $(x,\xi)\in V_0$. Here $b_{-m}\in S_h^{-m}(V_0)$ means that, in every local coordinate chart on $T^*X$, the coordinate representative of $b_{-m}$ satisfies the usual order $-m$ semiclassical symbol estimates on compact subsets of $V_0$. Equivalently, after possibly shrinking $V_0$, the principal symbol $a_m$ is nowhere zero on $V_0$ and its reciprocal belongs to this order $-m$ symbol class on that neighbourhood.
Choose an open neighbourhood $V\subset T^*X$ of $(x_0,\xi_0)$ with $\overline V\Subset V_0$. Let $C\in\Psi_h^0(X)$ satisfy
\begin{align*}
K:=\operatorname{WF}_h(C)\Subset V.
\end{align*}
Choose $C_1\in\Psi_h^0(X)$ such that $C_1$ is elliptic on an open neighbourhood $U_K\subset V_0$ of $K$ and such that $\operatorname{WF}_h(C_1)\Subset V_0$. This is possible by the standard cutoff construction in the semiclassical pseudodifferential calculus, applied to the compact set $K\Subset V_0$.
[/step]
[step:Construct a parametrix after inserting the cutoff $C_1$]
Let $c_1$ denote the scalar semiclassical principal symbol of $C_1$ on $U_K$. Since $C_1$ is elliptic on $U_K$ and $A$ is elliptic on $V_0$, the product symbol $c_1a_m$ is elliptic on $U_K$. Thus the composed operator $C_1A\in\Psi_h^m(X)$ is elliptic on a neighbourhood of $K=\operatorname{WF}_h(C)$.
We invoke the semiclassical elliptic parametrix theorem in the following form: if $P\in\Psi_h^m(X)$ is elliptic on an open set $U\subset T^*X$ and $C\in\Psi_h^0(X)$ satisfies $\operatorname{WF}_h(C)\Subset U$, then there exists $B\in\Psi_h^{-m}(X)$ such that $C-CBP\in h^\infty\Psi_h^{-\infty}(X)$. The residual class $h^\infty\Psi_h^{-\infty}(X)$ denotes operator families $Q_h:\mathcal E'(X)\to C^\infty(X)$ such that, for every Sobolev orders $r,t\in\mathbb R$ and every $N\in\mathbb N$, the operator norm of $Q_h:H_h^r(X)\to H_h^t(X)$ is bounded by $O(h^N)$ on one common interval $0<h<h_Q$, after restricting to compactly supported inputs when needed. The hypotheses hold with $P=C_1A$ and $U=U_K$, because $C_1A$ is elliptic on $U_K$ and $K=\operatorname{WF}_h(C)\Subset U_K$. Therefore there exists an operator $B\in\Psi_h^{-m}(X)$ such that
\begin{align*}
C - C B C_1 A \in h^\infty \Psi_h^{-\infty}(X).
\end{align*}
Define the remainder operator $R_h:\mathcal E'(X)\to C^\infty(X)$ by
\begin{align*}
R_h:=C-CBC_1A.
\end{align*}
Then
\begin{align*}
C u = C B C_1 A u + R_h u
\end{align*}
for every $h$-dependent compactly supported distribution $u=u_h\in\mathcal E'(X)$.
[guided]
The purpose of ellipticity is to construct an inverse only where $C$ observes the distribution. Define
\begin{align*}
K=\operatorname{WF}_h(C).
\end{align*}
From the previous step, $K\Subset V\Subset V_0$, the operator $A$ is elliptic on $V_0$, and $C_1$ is elliptic on an open neighbourhood $U_K\subset V_0$ of $K$.
We first fold the right cutoff into the operator to which the parametrix theorem will be applied. Let $c_1$ be the scalar semiclassical principal symbol of $C_1$ on $U_K$. Because $C_1$ is elliptic on $U_K$, $c_1$ has an order $0$ microlocal inverse there. Because $A$ is elliptic on $V_0$ and $U_K\subset V_0$, $a_m$ has an order $-m$ microlocal inverse on $U_K$. Hence the product symbol $c_1a_m$, which is the principal symbol of $C_1A\in\Psi_h^m(X)$, has an order $-m$ microlocal inverse on $U_K$. Therefore $C_1A$ is elliptic on $U_K$.
We now apply the semiclassical elliptic parametrix theorem to $P=C_1A$. In the form needed here, it requires an operator $P\in\Psi_h^m(X)$ elliptic on an open microlocal region $U$ and a left cutoff $C\in\Psi_h^0(X)$ with $\operatorname{WF}_h(C)\Subset U$. We take $U=U_K$. The ellipticity hypothesis holds by the product-symbol argument above. The microsupport hypothesis holds because $\operatorname{WF}_h(C)=K\Subset U_K$. The theorem therefore gives an operator $B\in\Psi_h^{-m}(X)$ such that
\begin{align*}
C - C B C_1 A \in h^\infty \Psi_h^{-\infty}(X).
\end{align*}
In this statement, $h^\infty\Psi_h^{-\infty}(X)$ denotes residual operator families $Q_h:\mathcal E'(X)\to C^\infty(X)$ whose Sobolev operator norms $Q_h:H_h^r(X)\to H_h^t(X)$ are $O(h^N)$ for every $r,t\in\mathbb R$ and every $N\in\mathbb N$ on a common sufficiently small interval of $h$.
The factor $C_1$ is not decorative: it localizes $A u$ to the same elliptic region in which the inverse symbol has been constructed. Since $C_1$ is elliptic on $K$, composing with $C_1$ does not discard the part of $A u$ needed to reconstruct $C u$ microlocally.
Define the residual operator $R_h:\mathcal E'(X)\to C^\infty(X)$ by
\begin{align*}
R_h:=C-CBC_1A.
\end{align*}
Then the operator identity $C=CBC_1A+R_h$ gives, for every $h$-dependent compactly supported distribution $u=u_h\in\mathcal E'(X)$,
\begin{align*}
C u = C B C_1 A u + R_h u.
\end{align*}
This is the mechanism of the estimate: $CBC_1A u$ is controlled by Sobolev boundedness of $CB$, and $R_hu$ is controlled by the residual class $h^\infty\Psi_h^{-\infty}(X)$.
[/guided]
[/step]
[step:Estimate the parametrix term by Sobolev boundedness]
Define the operator
\begin{align*}
T_h:=CB.
\end{align*}
Since $C\in\Psi_h^0(X)$ and $B\in\Psi_h^{-m}(X)$, the semiclassical composition calculus gives
\begin{align*}
T_h\in\Psi_h^{-m}(X).
\end{align*}
By the semiclassical Sobolev mapping estimate for pseudodifferential operators (citing a result not yet in the wiki: Semiclassical pseudodifferential Sobolev mapping estimate), $T_h$ extends to a bounded linear map
\begin{align*}
T_h:H_h^{s-m}(X)\to H_h^s(X),
\end{align*}
whose operator norm is bounded uniformly for all sufficiently small $h$ by finitely many semiclassical symbol seminorms of $T_h$. Therefore there exist constants $M>0$ and $h_1>0$, depending on $A$, $B$, $C$, $C_1$, $s$, and finitely many seminorms of the symbols but not on $h$, such that
\begin{align*}
\|C B C_1 A u\|_{H_h^s(X)} \leq M\|C_1 A u\|_{H_h^{s-m}(X)}
\end{align*}
for all $0<h<h_1$ whenever the norm on the right-hand side is finite.
[/step]
[step:Estimate the residual smoothing term with arbitrary powers of $h$]
Since
\begin{align*}
R_h\in h^\infty\Psi_h^{-\infty}(X),
\end{align*}
the definition of $h^\infty\Psi_h^{-\infty}(X)$ gives a number $h_2>0$, depending on the residual family $R_h$ but not on $N$, such that all residual Sobolev estimates hold on the common interval $0<h<h_2$. The semiclassical smoothing remainder estimate (citing a result not yet in the wiki: Semiclassical pseudodifferential calculus and smoothing remainders) then implies the following: for every $N\in\mathbb N$ and every $s\in\mathbb R$, there exists a constant $D_N>0$ such that
\begin{align*}
\|R_h u\|_{H_h^s(X)} \leq D_N h^N\|u\|_{H_h^{-N}(X)}
\end{align*}
for all $0<h<h_2$ and all compactly supported distributions $u=u_h\in\mathcal E'(X)$ with finite $H_h^{-N}(X)$ norm.
[/step]
[step:Combine the two estimates to obtain the microlocal elliptic bound]
Define
\begin{align*}
h_0:=\min\{h_1,h_2\}.
\end{align*}
This number is fixed before choosing $N$. Let $N\in\mathbb N$ be arbitrary. For $0<h<h_0$, the microlocal identity and the triangle inequality in $H_h^s(X)$ give
\begin{align*}
\|Cu\|_{H_h^s(X)} \leq \|C B C_1 A u\|_{H_h^s(X)}+\|R_hu\|_{H_h^s(X)}.
\end{align*}
Using the parametrix-term estimate and the smoothing-remainder estimate, we obtain
\begin{align*}
\|Cu\|_{H_h^s(X)} \leq M\|C_1Au\|_{H_h^{s-m}(X)}+D_Nh^N\|u\|_{H_h^{-N}(X)}.
\end{align*}
Set
\begin{align*}
C_N:=\max\{M,D_N\}.
\end{align*}
Then
\begin{align*}
\|Cu\|_{H_h^s(X)} \leq C_N\|C_1Au\|_{H_h^{s-m}(X)}+C_Nh^N\|u\|_{H_h^{-N}(X)}.
\end{align*}
This is the asserted microlocal elliptic estimate.
[/step]
