[proofplan]
The proof uses the standard calculus of wave front sets for pullbacks, products, and proper pushforwards. First we identify the wave front set of $\pi_Y^*f$ and check that the stated disjointness condition is exactly the product-transversality condition for $K\cdot \pi_Y^*f$. Then the product wave front estimate gives all possible covectors of the product on $X\times Y$. Finally the proper pushforward estimate for $\pi_X$ selects precisely those product covectors whose $Y$-component is zero, and the primed sign convention converts the two remaining alternatives into $C\circ \operatorname{WF}(f)$ and $\operatorname{WF}'_X(K)$.
[/proofplan]
[step:Identify the pullback wave front set of $\pi_Y^*f$]
Let
\begin{align*}
v:=\pi_Y^*f\in \mathcal D'(X\times Y)
\end{align*}
denote the pullback of $f$ by the projection $\pi_Y:X\times Y\to Y$. Since $\pi_Y$ is a smooth submersion, its differential is surjective at every point, so its pullback on covectors sends $(y,\eta)\in T^*Y$ to $(x,y;0,\eta)\in T^*_{(x,y)}(X\times Y)$. By the standard pullback theorem for wave front sets (citing a result not yet in the wiki: Pullback theorem for wave front sets),
\begin{align*}
\operatorname{WF}(v)\subset \{(x,y;0,\eta)\in T^*(X\times Y)\setminus 0:(y,\eta)\in \operatorname{WF}(f)\}.
\end{align*}
Here $0$ denotes the zero covector in $T_x^*X$.
[/step]
[step:Use the transversality hypothesis to define the product]
The product theorem for distributions (citing a result not yet in the wiki: Product theorem for distributions) requires that no point $(x,y)\in X\times Y$ and no nonzero covector $(\xi,\theta)\in T_x^*X\times T_y^*Y$ satisfy simultaneously
\begin{align*}
(x,y;\xi,\theta)\in \operatorname{WF}(K)\quad\text{and}\quad (x,y;-\xi,-\theta)\in \operatorname{WF}(v).
\end{align*}
By the previous step, the second condition can occur only when $-\xi=0$ and $(y,-\theta)\in \operatorname{WF}(f)$. Equivalently, the possible obstruction is a pair
\begin{align*}
(x,y;0,\theta)\in \operatorname{WF}(K)\quad\text{and}\quad (y,-\theta)\in \operatorname{WF}(f).
\end{align*}
Writing $\eta:=-\theta$, this obstruction is exactly
\begin{align*}
(x,y;0,-\eta)\in \operatorname{WF}(K)\quad\text{and}\quad (y,\eta)\in \operatorname{WF}(f),
\end{align*}
which, by the definition of $\operatorname{WF}'(K)$, is the same as
\begin{align*}
(x,0;y,\eta)\in \operatorname{WF}'(K)\quad\text{and}\quad (y,\eta)\in \operatorname{WF}(f).
\end{align*}
The assumed emptiness of $\operatorname{WF}'(K)\cap ((X\times \{0\})\times \operatorname{WF}(f))$ excludes exactly these obstructions. Therefore $K\cdot \pi_Y^*f$ is a well-defined distribution on $X\times Y$.
[guided]
We must check the product condition in the unprimed cotangent variables, because the product theorem is a theorem about distributions on the same manifold $X\times Y$. Set
\begin{align*}
v:=\pi_Y^*f.
\end{align*}
The pullback computation gives
\begin{align*}
\operatorname{WF}(v)\subset \{(x,y;0,\eta):(y,\eta)\in \operatorname{WF}(f)\}.
\end{align*}
Thus every covector in $\operatorname{WF}(v)$ has zero $X$-component.
The product theorem says that $K\cdot v$ is defined if there is no covector in $\operatorname{WF}(K)$ opposite to a covector in $\operatorname{WF}(v)$ at the same base point. So a forbidden pair would have the form
\begin{align*}
(x,y;\xi,\theta)\in \operatorname{WF}(K)
\end{align*}
and
\begin{align*}
(x,y;-\xi,-\theta)\in \operatorname{WF}(v).
\end{align*}
Since the second covector belongs to $\operatorname{WF}(v)$, its $X$-component must be zero. Hence $-\xi=0$, so $\xi=0$, and there is some $(y,\eta)\in \operatorname{WF}(f)$ with $-\theta=\eta$. Therefore the forbidden condition is precisely
\begin{align*}
(x,y;0,-\eta)\in \operatorname{WF}(K)\quad\text{with}\quad (y,\eta)\in \operatorname{WF}(f).
\end{align*}
The primed relation was defined by changing the sign of the $Y$-covector, so
\begin{align*}
(x,y;0,-\eta)\in \operatorname{WF}(K)
\end{align*}
is equivalent to
\begin{align*}
(x,0;y,\eta)\in \operatorname{WF}'(K).
\end{align*}
Thus the hypothesis
\begin{align*}
\operatorname{WF}'(K)\cap ((X\times \{0\})\times \operatorname{WF}(f))=\varnothing
\end{align*}
is exactly the product-transversality hypothesis. This proves that $K\cdot \pi_Y^*f$ is defined.
[/guided]
[/step]
[step:Estimate the wave front set of the product]
Let
\begin{align*}
w:=K\cdot \pi_Y^*f\in \mathcal D'(X\times Y).
\end{align*}
The product wave front estimate gives
\begin{align*}
\operatorname{WF}(w)\subset \operatorname{WF}(K)\cup \operatorname{WF}(v)\cup (\operatorname{WF}(K)+\operatorname{WF}(v)),
\end{align*}
where the fiberwise sum is defined by
\begin{align*}
\operatorname{WF}(K)+\operatorname{WF}(v):=\{(x,y;\xi_1+\xi_2,\theta_1+\theta_2):(x,y;\xi_1,\theta_1)\in \operatorname{WF}(K),\ (x,y;\xi_2,\theta_2)\in \operatorname{WF}(v)\}.
\end{align*}
Using the pullback estimate for $v$, any element of this sum that has total covector $(\xi,0)$ must arise from covectors
\begin{align*}
(x,y;\xi,\theta)\in \operatorname{WF}(K)\quad\text{and}\quad (x,y;0,\eta)\in \operatorname{WF}(v)
\end{align*}
with $\theta+\eta=0$. Hence $(y,\eta)\in \operatorname{WF}(f)$ and
\begin{align*}
(x,y;\xi,-\eta)\in \operatorname{WF}(K),
\end{align*}
which is equivalent to
\begin{align*}
(x,\xi;y,\eta)\in \operatorname{WF}'(K).
\end{align*}
[/step]
[step:Apply the proper pushforward estimate along $\pi_X$]
The support of $w$ is contained in
\begin{align*}
\operatorname{supp}K\cap (X\times \operatorname{supp}f),
\end{align*}
because $v=\pi_Y^*f$ has support contained in $X\times \operatorname{supp}f$. By hypothesis, $\pi_X$ is proper on this closed support set. Therefore the pushforward
\begin{align*}
Tf=(\pi_X)_*w
\end{align*}
is a well-defined distribution in $\mathcal D'(X)$.
By the standard proper pushforward theorem for wave front sets (citing a result not yet in the wiki: Pushforward theorem for wave front sets),
\begin{align*}
\operatorname{WF}(Tf)\subset \{(x,\xi)\in T^*X\setminus 0:\text{ there exists }y\in Y\text{ with }(x,y;\xi,0)\in \operatorname{WF}(w)\}.
\end{align*}
Fix $(x,\xi)\in \operatorname{WF}(Tf)$. Then there exists $y\in Y$ such that $(x,y;\xi,0)\in \operatorname{WF}(w)$. The product estimate gives three alternatives.
First, if $(x,y;\xi,0)\in \operatorname{WF}(K)$, then by the primed convention
\begin{align*}
(x,\xi;y,0)\in \operatorname{WF}'(K),
\end{align*}
so $(x,\xi)\in \operatorname{WF}'_X(K)$.
Second, $(x,y;\xi,0)$ cannot come from $\operatorname{WF}(v)$ alone, because every covector in $\operatorname{WF}(v)$ has zero $X$-component, while $(x,\xi)\in T^*X\setminus 0$.
Third, if $(x,y;\xi,0)$ comes from $\operatorname{WF}(K)+\operatorname{WF}(v)$, then the previous step gives some $(y,\eta)\in \operatorname{WF}(f)$ such that
\begin{align*}
(x,\xi;y,\eta)\in \operatorname{WF}'(K).
\end{align*}
Since $(x,\xi)\in T^*X\setminus 0$ and $(y,\eta)\in \operatorname{WF}(f)\subset T^*Y\setminus 0$, this point lies in $C$. Hence
\begin{align*}
(x,\xi)\in C\circ \operatorname{WF}(f).
\end{align*}
[/step]
[step:Combine the alternatives]
Every covector $(x,\xi)\in \operatorname{WF}(Tf)$ belongs either to $\operatorname{WF}'_X(K)$ or to $C\circ \operatorname{WF}(f)$. Therefore
\begin{align*}
\operatorname{WF}(Tf)\subset C\circ \operatorname{WF}(f)\cup \operatorname{WF}'_X(K).
\end{align*}
This is the claimed wave front set mapping inclusion.
[/step]
