[proofplan]
The image measure formula is a direct restatement of the [Change of Variables for Lipschitz Maps](/theorems/3076) with the test function $g$ taken to be the indicator $\mathbf{1}_B$ of an arbitrary Borel set $B \subseteq \mathbb{R}^n$. Step 1 verifies that the hypotheses of the change of variables theorem are met by the present setup. Step 2 substitutes $g = \mathbf{1}_B$ into the change of variables formula and identifies both sides with the desired pushforward identity. The argument is short because all the analytic content (approximation by simple functions, monotone convergence, the area formula) has already been packaged into Theorem 3076.
[/proofplan]
[step:Verify the hypotheses of the change of variables formula]
The map
\begin{align*}
f: \mathbb{R}^m &\to \mathbb{R}^n
\end{align*}
is Lipschitz with $m \le n$, and $A \subseteq \mathbb{R}^m$ is $\mathcal{L}^m$-measurable with $f$ injective on $A$, by the hypotheses of the present theorem. These are precisely the structural hypotheses of the [Change of Variables for Lipschitz Maps](/theorems/3076).
For any Borel set $B \subseteq \mathbb{R}^n$, define the test function
\begin{align*}
g_B: \mathbb{R}^n &\to [0, +\infty] \\
y &\mapsto \mathbf{1}_B(y).
\end{align*}
The function $g_B$ is $\mathcal{H}^m$-measurable: indicator functions of Borel sets are Borel measurable, and Borel measurable functions are $\mathcal{H}^m$-measurable since $\mathcal{H}^m$ is a Borel-regular measure. Hence $g_B$ is admissible as the test function in Theorem 3076.
[/step]
[step:Apply the change of variables formula with $g = \mathbf{1}_B$]
The change of variables formula applied to $g_B$ gives
\begin{align*}
\int_A \mathbf{1}_B(f(x)) \, J_m f(x) \, d\mathcal{L}^m(x) = \int_{f(A)} \mathbf{1}_B(y) \, d\mathcal{H}^m(y).
\end{align*}
We simplify each side.
**Left-hand side**: for $x \in A$, the value $\mathbf{1}_B(f(x))$ is $1$ when $f(x) \in B$ and $0$ otherwise. Since the integration is over $A$,
\begin{align*}
\mathbf{1}_B(f(x)) = \mathbf{1}_{f^{-1}(B)}(x) \qquad \text{for } x \in A.
\end{align*}
Restricting to $A$, the indicator $\mathbf{1}_{f^{-1}(B)}$ on $A$ equals the indicator of the set $f^{-1}(B) \cap A$, so
\begin{align*}
\int_A \mathbf{1}_B(f(x)) \, J_m f(x) \, d\mathcal{L}^m(x) = \int_{f^{-1}(B) \cap A} J_m f(x) \, d\mathcal{L}^m(x).
\end{align*}
The set $f^{-1}(B) \cap A$ is $\mathcal{L}^m$-measurable: $f$ is continuous (Lipschitz implies continuous), so $f^{-1}(B)$ is Borel measurable, and the intersection with the $\mathcal{L}^m$-measurable set $A$ is again $\mathcal{L}^m$-measurable.
**Right-hand side**: integrating an indicator over a set gives the measure of the intersection,
\begin{align*}
\int_{f(A)} \mathbf{1}_B(y) \, d\mathcal{H}^m(y) = \mathcal{H}^m(B \cap f(A)).
\end{align*}
Combining,
\begin{align*}
\int_{f^{-1}(B) \cap A} J_m f \, d\mathcal{L}^m = \mathcal{H}^m(B \cap f(A)).
\end{align*}
This is precisely the integral identity in the theorem statement. Reading the identity as a statement about measures: the left side is the value at $B$ of the pushforward measure $f_\#(J_m f \cdot \mathcal{L}^m \lfloor A)$, since by definition of pushforward
\begin{align*}
f_\#(J_m f \cdot \mathcal{L}^m \lfloor A)(B) = \int_{f^{-1}(B)} J_m f \cdot \mathbf{1}_A \, d\mathcal{L}^m = \int_{f^{-1}(B) \cap A} J_m f \, d\mathcal{L}^m,
\end{align*}
and the right side is the value at $B$ of the restricted Hausdorff measure $\mathcal{H}^m \lfloor f(A)$ since $(\mathcal{H}^m \lfloor f(A))(B) = \mathcal{H}^m(B \cap f(A))$. Hence
\begin{align*}
f_\#(J_m f \cdot \mathcal{L}^m \lfloor A) = \mathcal{H}^m \lfloor f(A)
\end{align*}
as Borel measures on $\mathbb{R}^n$, which is the image measure formula.
[/step]
