Pushforward measure integral property Let $\mu$ be a Borel measure on $X$ and $T: X \rightarrow Y$ a Borel map ($Y$ topological space). I define $$ T _* \mu(E) = \mu(T^{-1}(E))  \qquad \forall E \subset Y \quad \text{Borel} $$
It is easy to prove that $T_* \mu$ is a measure on $Y$. But why, if $f : Y \rightarrow \mathbb{R}$ is $L^1(T_* \mu)$,
$$ \int_Y f \ d T_* \mu = \int_X f \circ T \ d \mu$$
First consider $f=1_E$ for some Borel set $E \subseteq Y$. Note that $$1_{T^{-1}(E)}(x)= 1 \Leftrightarrow x \in T^{-1}(E) \Leftrightarrow T(x) \in E \Leftrightarrow 1_{E}(T(x))=1 \tag{1} $$
Thus $$\int_Y f \, dT_{\ast} \mu = T_{\ast} \mu(E) \stackrel{\text{def}}{=} \mu(T^{-1}(E)) = \int 1_{T^{-1}(E)}(x) \, d\mu(x) \\ \stackrel{(1)}{=} \int 1_E (T(x)) \, d\mu(x) = \int_X f \circ T \, d\mu$$ so the assertion holds for all $f$ of the form $f=1_E$.
By linearity, we conclude $$\int_Y f \, dT_{\ast} \mu = \int_X f \circ T \, d\mu \tag{2}$$ for all $$f = \sum_{j=1}^n c_j \cdot 1_{E_j}$$ for some $n \in \mathbb{N}$, $c_j \in \mathbb{R}$, $E_j \subseteq Y$ Borel. This means that the formula holds for all simple functions.
Let $f \in L^1(T_{\ast} \mu)$ such that $f \geq 0$. Then there exists a sequence $(f_n)_n$ of simple functions such that $f = \sup_n f_n$. Thus, we obtain by monotone convergence $$\int f \, dT_{\ast} \mu = \sup_n \int f_n \, dT_{\ast} \mu = \sup_n \int f_n \circ T \, d\mu = \int f \circ T \, d\mu$$
For arbritrary $f \in L^1(T_{\ast} \mu)$, we write $f$ as a sum, $f = f^+ - f^-$ where $f^+, f^- \geq 0$ and $f^-, f^+ \in L^1(T_{\ast} \mu)$. By 3. the assertion holds for $f^-$ and $f^+$, so the assertion follows easily for $f$ using the linearity of the integral.
It is true for the characteristic functions, so it is true for any measurable function.