[proofplan]
We start from the normalized [Weyl integration formula](/theorems/9714) on the maximal torus, which applies to the measurable $\mu_G$-integrable class function $f$ and supplies both the weighted torus integrability of $t\mapsto f(t)D(t)$ and the formula with the factor $1/|W|$. The main point is to show that this weighted integrand is $W$-invariant: this uses conjugation-invariance of $f$ and the fact that the Weyl group permutes the roots while the product defining $D$ may be rewritten over unordered root pairs. A finite-group fundamental-domain decomposition then rewrites the integral over $T$ as $|W|$ times the integral over $C$, cancelling the factor in the Weyl integration formula.
[/proofplan]
[step:Rewrite the Weyl denominator as a product over root pairs]
Let $\Phi/\{\pm 1\}$ denote the set of unordered pairs $\{\alpha,-\alpha\}$ with $\alpha\in\Phi$. Since $\Phi^+$ contains exactly one root from each pair $\{\alpha,-\alpha\}$, and since $-\alpha$ corresponds to the inverse character $\alpha^{-1}:T\to S^1$, we have, for every $t\in T$,
\begin{align*}
D(t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-\alpha(t)|^2.
\end{align*}
This expression is independent of the choice of representative of the pair. Indeed, if $\alpha(t)\in S^1$, then
\begin{align*}
|1-\alpha(t)^{-1}|=|\alpha(t)^{-1}||\alpha(t)-1|=|1-\alpha(t)|.
\end{align*}
Thus replacing $\alpha$ by $-\alpha$ does not change the factor.
[/step]
[step:Prove that the weighted torus integrand is invariant under the Weyl group]
Define the [measurable function](/page/Measurable%20Function) $F:T\to\mathbb C$ by $F(t):=f(t)D(t)$. We prove that $F$ is $W$-invariant. Let $w\in W$, and choose a representative $n\in N_G(T)$ of $w$. The Weyl [group action](/page/Group%20Action) is given by
\begin{align*}
w\cdot t=ntn^{-1}.
\end{align*}
Since $f$ is a class function on $G$,
\begin{align*}
f(w\cdot t)=f(ntn^{-1})=f(t).
\end{align*}
It remains to check the density. The Weyl group acts on $\Phi$ by
\begin{align*}
(w\alpha)(t):=\alpha(w^{-1}\cdot t),
\end{align*}
and this action permutes the unordered pairs $\{\alpha,-\alpha\}$. Using the root-pair expression for $D$,
\begin{align*}
D(w\cdot t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-\alpha(w\cdot t)|^2.
\end{align*}
As $\{\alpha,-\alpha\}$ runs through $\Phi/\{\pm 1\}$, so does $\{w^{-1}\alpha,-w^{-1}\alpha\}$. Therefore the product is unchanged, and
\begin{align*}
D(w\cdot t)=D(t).
\end{align*}
Hence
\begin{align*}
F(w\cdot t)=F(t)
\end{align*}
for every $w\in W$ and every $t\in T$.
[guided]
We need the function integrated over the torus to be constant on Weyl orbits, because the next step replaces the torus by one representative chamber. Define the measurable function $F:T\to\mathbb C$ by $F(t):=f(t)D(t)$. We verify $F(w\cdot t)=F(t)$ for each $w\in W$.
Choose $w\in W$ and choose an element $n\in N_G(T)$ whose coset in $N_G(T)/T$ is $w$. By definition of the Weyl action on $T$,
\begin{align*}
w\cdot t=ntn^{-1}.
\end{align*}
Since $f:G\to\mathbb C$ is a class function, it is invariant under conjugation in $G$. Therefore
\begin{align*}
f(w\cdot t)=f(ntn^{-1})=f(t).
\end{align*}
Now we check the Weyl denominator. The subtle point is that $w$ need not preserve the chosen positive roots $\Phi^+$, so we should not argue directly with the positive-root product. Instead, we use the equivalent product over unordered pairs $\{\alpha,-\alpha\}$. This is legitimate because $\Phi^+$ contains exactly one root from each such pair, and for $z=\alpha(t)\in S^1$,
\begin{align*}
|1-z^{-1}|=|z^{-1}||z-1|=|1-z|.
\end{align*}
Thus the factor attached to $\alpha$ is the same as the factor attached to $-\alpha$.
The Weyl group permutes the root system $\Phi$, and therefore it permutes the set of unordered pairs $\Phi/\{\pm 1\}$. With the induced action on roots defined by $(u\alpha)(s):=\alpha(u^{-1}\cdot s)$ for $u\in W$ and $s\in T$, we have
\begin{align*}
\alpha(w\cdot t)=(w^{-1}\alpha)(t).
\end{align*}
Hence
\begin{align*}
D(w\cdot t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-(w^{-1}\alpha)(t)|^2.
\end{align*}
As $\{\alpha,-\alpha\}$ runs through $\Phi/\{\pm 1\}$, the pair $\{w^{-1}\alpha,-w^{-1}\alpha\}$ also runs through $\Phi/\{\pm 1\}$. Therefore this is the same product as
\begin{align*}
D(t)=\prod_{\{\alpha,-\alpha\}\in \Phi/\{\pm 1\}} |1-\alpha(t)|^2,
\end{align*}
only with the factors reindexed. Therefore
\begin{align*}
D(w\cdot t)=D(t).
\end{align*}
Combining this with the class-function identity gives
\begin{align*}
F(w\cdot t)=f(w\cdot t)D(w\cdot t)=f(t)D(t)=F(t).
\end{align*}
[/guided]
[/step]
[step:Apply the normalized Weyl integration formula to obtain torus integrability]
Apply the normalized Weyl integration formula [citetheorem:9714] to the $\mu_G$-integrable measurable class function $f:G\to\mathbb C$. Its measurable $L^1$ hypotheses are exactly the compact connected Lie group $G$, the maximal torus $T$, the normalized Haar probability measures $\mu_G$ and $\mu_T$, the chosen positive root system $\Phi^+$, and the assumption that $f$ is a $\mu_G$-integrable measurable class function. Therefore the function $F:T\to\mathbb C$, $t\mapsto f(t)D(t)$, is $\mu_T$-integrable and
\begin{align*}
\int_G f(g)\,d\mu_G(g)=\frac{1}{|W|}\int_T F(t)\,d\mu_T(t).
\end{align*}
[/step]
[step:Replace the torus integral by the chamber integral]
By the fundamental-domain hypothesis, there exists a measurable $\mu_T$-null set $E\subset T$ such that
\begin{align*}
T\setminus E=\bigsqcup_{w\in W}w(C\setminus E).
\end{align*}
Since Haar measure on $T$ is invariant under the continuous automorphisms induced by $W$, for each $w\in W$ one has
\begin{align*}
\int_{w(C\setminus E)}F(t)\,d\mu_T(t)=\int_{C\setminus E}F(w\cdot t)\,d\mu_T(t).
\end{align*}
Using $W$-invariance of $F$,
\begin{align*}
\int_{w(C\setminus E)}F(t)\,d\mu_T(t)=\int_{C\setminus E}F(t)\,d\mu_T(t).
\end{align*}
Summing over the disjoint decomposition of $T\setminus E$ gives
\begin{align*}
\int_T F(t)\,d\mu_T(t)=\sum_{w\in W}\int_{w(C\setminus E)}F(t)\,d\mu_T(t).
\end{align*}
Therefore
\begin{align*}
\int_T F(t)\,d\mu_T(t)=|W|\int_{C\setminus E}F(t)\,d\mu_T(t).
\end{align*}
Because $E$ is $\mu_T$-null and $F$ is $\mu_T$-integrable, this is
\begin{align*}
\int_T f(t)D(t)\,d\mu_T(t)=|W|\int_C f(t)D(t)\,d\mu_T(t).
\end{align*}
[/step]
[step:Substitute the chamber identity into the normalized Weyl integration formula]
From the earlier application of the normalized Weyl integration formula [citetheorem:9714],
\begin{align*}
\int_G f(g)\,d\mu_G(g)=\frac{1}{|W|}\int_T f(t)D(t)\,d\mu_T(t).
\end{align*}
Using the chamber identity from the preceding step,
\begin{align*}
\int_T f(t)D(t)\,d\mu_T(t)=|W|\int_C f(t)D(t)\,d\mu_T(t).
\end{align*}
Substitution gives
\begin{align*}
\int_G f(g)\,d\mu_G(g)=\frac{1}{|W|}|W|\int_C f(t)D(t)\,d\mu_T(t).
\end{align*}
Since $W$ is finite and nonempty, $|W|\ge 1$, and cancellation yields
\begin{align*}
\int_G f(g)\,d\mu_G(g)=\int_C f(t)D(t)\,d\mu_T(t).
\end{align*}
This is the claimed Weyl chamber form of the Weyl integration formula.
[/step]
