Invariance of the hyperbolic area measure under Möbius maps (change of variables on the upper half-plane)

Let $\sigma=\begin{pmatrix}a&b\\c&d\end{pmatrix}\in SL_2(\mathbf Z)$ act on the upper half-plane $\mathfrak H=\{z:\operatorname{Im}z>0\}$ by $\sigma z=(az+b)/(cz+d)$, and let $T\subset\mathfrak H$ be a Lebesgue-measurable set. Then for every $G:\mathbf C\to\mathbf C$,

This is the $SL_2(\mathbf R)$-invariance of the hyperbolic area measure $y^{-2}dx\,dy$, in the form of a change of variables for the Lebesgue set integral: the map $z\mapsto\sigma z$ is injective on $\mathfrak H$ with complex derivative $(cz+d)^{-2}$, so its real Jacobian determinant is $|cz+d|^{-4}$, while $\operatorname{Im}(\sigma z)=\operatorname{Im}z/|cz+d|^{2}$; the two factors cancel. It lets one pull an integral over an $SL_2(\mathbf Z)$-translate of the standard fundamental-domain tile back to the tile itself, which is how Petersson integrals over a fundamental domain of a finite-index subgroup are reduced to integrals over the level-one tile.

Formalization Note The integrals are Bochner set integrals for the Lebesgue measure on $\mathbf C$; no integrability hypothesis is needed since the identity is an instance of Mathlib's change-of-variables theorem integral_image_eq_integral_abs_det_fderiv_smul. The auxiliary Lebesgue-Jacobian form $\int_{\sigma T}F=\int_T|cz+d|^{-4}F(\sigma z)$ and the determinant of complex multiplication (det (c • 1) = |c|^2 as an $\mathbf R$-linear map of $\mathbf C$) are proved along the way.