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

[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: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]