[proofplan] We first separate the elements of the maximal torus on which no root takes the value $1$ from the singular root hypertori, and we show that the singular contribution has measure zero. On the resulting regular locus, the conjugation map from the torus together with conjugating cosets is a smooth covering of degree $|W|$, and its absolute Jacobian is the Weyl density $D(t)$. The change-of-variables formula therefore gives the identity for continuous class functions. Finally, the two sides define the same positive measure on the conjugacy quotient, so the identity extends from continuous class functions to all integrable conjugation-invariant representatives. [/proofplan]

[step:Remove the singular part of the maximal torus and of the group]Define the regular part of $T$ by \begin{align*} T_{\mathrm{reg}}:=\{t\in T:\alpha(t)\ne 1\text{ for every }\alpha\in R\}. \end{align*} Its complement is \begin{align*} T\setminus T_{\mathrm{reg}}=\bigcup_{\alpha\in R}\ker \alpha . \end{align*} For every non-zero root $\alpha\in R$, the character $\alpha:T\to S^1$ is non-trivial, so $\ker\alpha$ is a proper closed subgroup of $T$. Its identity component $H_\alpha:=(\ker\alpha)^\circ$ is a compact connected subtorus of $T$ of dimension strictly smaller than $\dim T$, and the compact Lie group $\ker\alpha/H_\alpha$ is finite. Thus $\ker\alpha$ is a finite disjoint union of cosets of $H_\alpha$, and each such coset has $\mu_T$-measure zero. Since $R$ is finite, $T\setminus T_{\mathrm{reg}}$ has $\mu_T$-measure zero. Define the regular part of $G$ by \begin{align*} G_{\mathrm{reg}}:=\{gtg^{-1}:g\in G,\ t\in T_{\mathrm{reg}}\}. \end{align*} By [citetheorem:9713], every element of $G$ is conjugate to an element of $T$, so \begin{align*} G\setminus G_{\mathrm{reg}} \end{align*} is the conjugation-saturation of $T\setminus T_{\mathrm{reg}}$. For each $\alpha\in R$, write $\ker\alpha$ as a finite disjoint union of cosets $C_{\alpha,j}=a_{\alpha,j}H_\alpha$, where $a_{\alpha,j}\in\ker\alpha$ and $H_\alpha=(\ker\alpha)^\circ$ is the compact connected subtorus defined above. Each coset $C_{\alpha,j}$ is a compact embedded submanifold of $T$ of dimension strictly smaller than $\dim T$. Define the smooth map $\Psi_{\alpha,j}:G/T\times C_{\alpha,j}\to G$ by \begin{align*} \Psi_{\alpha,j}(gT,t):=gtg^{-1}. \end{align*} The domain $G/T\times C_{\alpha,j}$ has dimension \begin{align*} \dim(G/T)+\dim C_{\alpha,j}<\dim(G/T)+\dim T=\dim G. \end{align*} In smooth coordinate charts, the image of a compact smooth manifold of dimension strictly smaller than $\dim G$ under a smooth map into $G$ has zero $\mu_G$-measure. Since \begin{align*} G\setminus G_{\mathrm{reg}}\subseteq \bigcup_{\alpha\in R}\bigcup_j \Psi_{\alpha,j}(G/T\times C_{\alpha,j}) \end{align*} and the union is finite, we obtain \begin{align*} \mu_G(G\setminus G_{\mathrm{reg}})=0. \end{align*} Moreover $D(t)=0$ for every $t\in T\setminus T_{\mathrm{reg}}$, since at least one factor $|1-\alpha(t)|^2$ vanishes.[/step]

[guided]The role of the regular set is to isolate the points where conjugation by $G$ has the expected finite Weyl-group ambiguity. We define \begin{align*} T_{\mathrm{reg}}:=\{t\in T:\alpha(t)\ne 1\text{ for every }\alpha\in R\}. \end{align*} A point of $T$ is singular exactly when at least one root character takes the value $1$, so \begin{align*} T\setminus T_{\mathrm{reg}}=\bigcup_{\alpha\in R}\ker \alpha . \end{align*} Each root $\alpha:T\to S^1$ is a non-trivial continuous character. Therefore $\ker\alpha$ is a proper closed subgroup of $T$. Its identity component $H_\alpha:=(\ker\alpha)^\circ$ is a compact connected subtorus of $T$ of dimension strictly smaller than $\dim T$, and the quotient compact Lie group $\ker\alpha/H_\alpha$ is finite. Hence $\ker\alpha$ is a finite disjoint union of cosets of $H_\alpha$. Each coset is a translate of a lower-dimensional compact submanifold of $T$, so it has zero Haar measure inside $T$. Since the root system $R$ is finite, the finite union $T\setminus T_{\mathrm{reg}}$ also has $\mu_T$-measure zero. Now define \begin{align*} G_{\mathrm{reg}}:=\{gtg^{-1}:g\in G,\ t\in T_{\mathrm{reg}}\}. \end{align*} The [maximal torus theorem](/theorems/9713) [citetheorem:9713] says that every element of $G$ is conjugate to some element of $T$. Thus the complement $G\setminus G_{\mathrm{reg}}$ is precisely the conjugation-saturation of the singular part $T\setminus T_{\mathrm{reg}}$. Why is this still a null set in $G$? Fix $\alpha\in R$. Write $\ker\alpha$ as the finite disjoint union of cosets $C_{\alpha,j}=a_{\alpha,j}H_\alpha$, where $a_{\alpha,j}\in\ker\alpha$ and $H_\alpha=(\ker\alpha)^\circ$. Each $C_{\alpha,j}$ is a compact embedded submanifold of $T$ of dimension strictly smaller than $\dim T$. For such a coset define the smooth map $\Psi_{\alpha,j}:G/T\times C_{\alpha,j}\to G$ by \begin{align*} \Psi_{\alpha,j}(gT,t):=gtg^{-1}. \end{align*} This map is smooth, and its domain has dimension \begin{align*} \dim(G/T)+\dim C_{\alpha,j}<\dim(G/T)+\dim T=\dim G. \end{align*} A smooth image of a compact manifold of dimension strictly smaller than the target manifold has zero measure with respect to any smooth volume measure on the target; this follows in coordinate charts from the usual local measure-zero theorem for smooth maps from lower-dimensional Euclidean domains. The singular conjugacy-saturation is contained in the finite union of the images of the maps $\Psi_{\alpha,j}$, so finite subadditivity gives \begin{align*} \mu_G(G\setminus G_{\mathrm{reg}})=0. \end{align*} Finally, the same vanishing factor shows that \begin{align*} D(t)=\prod_{\alpha\in R^+}|1-\alpha(t)|^2=0 \end{align*} for every $t\in T\setminus T_{\mathrm{reg}}$.[/guided]

[step:Apply the regular conjugation covering and its Jacobian] Define the regular conjugation map $\Phi_{\mathrm{reg}}:G/T\times T_{\mathrm{reg}}\to G_{\mathrm{reg}}$ by \begin{align*} \Phi_{\mathrm{reg}}(gT,t):=gtg^{-1}. \end{align*} The hypotheses of [citetheorem:9744] are satisfied: $G$ is compact and connected, $T$ is a maximal torus, and $T_{\mathrm{reg}}$ and $G_{\mathrm{reg}}$ are exactly the regular loci defined above from the root system $R$. Hence $\Phi_{\mathrm{reg}}$ is a smooth covering map of degree $|W|$. Let $\mu_{G/T}$ be the quotient probability measure induced by $\mu_G$ on $G/T$. The hypotheses of [citetheorem:9746] are also satisfied with these normalized Haar measures and the quotient measure on $G/T$, so the absolute Jacobian of $\Phi_{\mathrm{reg}}$ at $(gT,t)$ is \begin{align*} D(t)=\prod_{\alpha\in R^+}|1-\alpha(t)|^2 . \end{align*} Let $F:G_{\mathrm{reg}}\to[0,\infty]$ be a non-negative Borel function. The map $(gT,t)\mapsto F(\Phi_{\mathrm{reg}}(gT,t))D(t)$ is Borel and non-negative because $\Phi_{\mathrm{reg}}$ is smooth and $D$ is Borel. Applying the change-of-variables formula for a finite covering and then Tonelli's theorem gives \begin{align*} \int_{G_{\mathrm{reg}}}F(x)\,d\mu_G(x)=\frac{1}{|W|}\int_{G/T}\int_{T_{\mathrm{reg}}}F(gtg^{-1})D(t)\,d\mu_T(t)\,d\mu_{G/T}(gT). \end{align*} The same identity holds for every integrable complex-valued Borel function $F$ by applying the non-negative identity separately to the positive and negative parts of $\operatorname{Re}F$ and $\operatorname{Im}F$. [/step]

[step:Evaluate the formula on continuous conjugation-invariant functions] Let $f:G\to\mathbb C$ be continuous and conjugation-invariant. Since $\mu_G(G\setminus G_{\mathrm{reg}})=0$, \begin{align*} \int_G f(x)\,d\mu_G(x)=\int_{G_{\mathrm{reg}}}f(x)\,d\mu_G(x). \end{align*} Applying the preceding step with $F=f|_{G_{\mathrm{reg}}}$ gives \begin{align*} \int_G f(x)\,d\mu_G(x)=\frac{1}{|W|}\int_{G/T}\int_{T_{\mathrm{reg}}}f(gtg^{-1})D(t)\,d\mu_T(t)\,d\mu_{G/T}(gT). \end{align*} Because $f$ is conjugation-invariant, \begin{align*} f(gtg^{-1})=f(t) \end{align*} for every $g\in G$ and every $t\in T_{\mathrm{reg}}$. Since $\mu_{G/T}$ is a probability measure, the $G/T$ integral contributes the factor $1$. Hence \begin{align*} \int_G f(x)\,d\mu_G(x)=\frac{1}{|W|}\int_{T_{\mathrm{reg}}}f(t)D(t)\,d\mu_T(t). \end{align*} As $D=0$ on $T\setminus T_{\mathrm{reg}}$, this is \begin{align*} \int_G f(x)\,d\mu_G(x)=\frac{1}{|W|}\int_T f(t)D(t)\,d\mu_T(t). \end{align*} [/step]

[step:Extend the identity to integrable conjugation-invariant representatives] Let $q:G\to G/\operatorname{Ad}(G)$ denote the measurable quotient map sending $g\in G$ to its [conjugacy class](/page/Conjugacy%20Class). Define two finite positive measures $\nu_1$ and $\nu_2$ on the conjugacy quotient by \begin{align*} \nu_1(A):=\mu_G(q^{-1}(A)), \end{align*} and \begin{align*} \nu_2(A):=\frac{1}{|W|}\int_{T\cap q^{-1}(A)}D(t)\,d\mu_T(t) \end{align*} for every Borel subset $A\subset G/\operatorname{Ad}(G)$. Since $q$ is continuous for the topological quotient and the inclusion $T\hookrightarrow G$ is continuous, the set $T\cap q^{-1}(A)$ is Borel in $T$, so $\nu_2$ is well-defined. The identity proved for continuous conjugation-invariant functions says exactly that \begin{align*} \int_{G/\operatorname{Ad}(G)}\varphi(C)\,d\nu_1(C)=\int_{G/\operatorname{Ad}(G)}\varphi(C)\,d\nu_2(C) \end{align*} for every [continuous function](/page/Continuous%20Function) $\varphi:G/\operatorname{Ad}(G)\to\mathbb C$. Since $G/\operatorname{Ad}(G)$ is compact Hausdorff, equality on continuous functions implies $\nu_1=\nu_2$. Now let $f:G\to\mathbb C$ be $\mu_G$-integrable and let $\tilde f:G\to\mathbb C$ be a conjugation-invariant measurable representative of its equivalence class. Because $G$ is compact metrizable and conjugacy classes are compact, the topological quotient $G/\operatorname{Ad}(G)$ is a compact [metrizable space](/page/Metrizable%20Space) and its Borel $\sigma$-algebra is the quotient Borel $\sigma$-algebra for $q$. Since $\tilde f$ is Borel measurable and constant on every conjugacy class, the set function \begin{align*} \bar f:G/\operatorname{Ad}(G)&\to\mathbb C \end{align*} defined by choosing any $g\in C$ and setting $\bar f(C):=\tilde f(g)$ is well-defined. For every [open set](/page/Open%20Set) $U\subset\mathbb C$, \begin{align*} q^{-1}(\bar f^{-1}(U))=\tilde f^{-1}(U), \end{align*} so the quotient definition of the Borel structure implies that $\bar f$ is measurable, and \begin{align*} \tilde f=\bar f\circ q. \end{align*} Since $\nu_1=\nu_2$, integrability of $\bar f$ with respect to $\nu_1$ is equivalent to integrability with respect to $\nu_2$, and \begin{align*} \int_G \tilde f(g)\,d\mu_G(g)=\int_{G/\operatorname{Ad}(G)}\bar f(C)\,d\nu_1(C)=\int_{G/\operatorname{Ad}(G)}\bar f(C)\,d\nu_2(C). \end{align*} By the definition of $\nu_2$, the last integral is \begin{align*} \frac{1}{|W|}\int_T \tilde f(t)D(t)\,d\mu_T(t). \end{align*} Therefore \begin{align*} \int_G \tilde f(g)\,d\mu_G(g)=\frac{1}{|W|}\int_T \tilde f(t)D(t)\,d\mu_T(t). \end{align*} This proves the Weyl integration formula for every conjugation-invariant measurable representative of the given $L^1$ class. If two such representatives differ on a $\mu_G$-null set, then their quotient functions agree $\nu_1$-almost everywhere, hence also $\nu_2$-almost everywhere; therefore the right-hand side is independent of the chosen conjugation-invariant representative. [/step]