[proofplan] The strategy bootstraps the change-of-variables form of the coarea formula from the basic [Coarea Formula](/theorems/3078) by approximating $g$ with simple functions and applying the basic formula to each level set in turn. Step 1 establishes the formula for $g = \mathbf{1}_E$ where $E \subseteq \mathbb{R}^n$ is $\mathcal{L}^n$-measurable, by recognising the basic coarea formula applied to the set $A \cap E$. Step 2 extends to non-negative simple functions by linearity. Step 3 extends to general non-negative measurable $g$ via monotone approximation by simple functions and the Monotone Convergence Theorem on both sides. The slicing measurability of $t \mapsto \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k}$ — needed to even state the right-hand side — emerges as part of the construction. [/proofplan]

[step:Establish the formula for $g = \mathbf{1}_E$ with $E \subseteq \mathbb{R}^n$ measurable] Let $E \subseteq \mathbb{R}^n$ be $\mathcal{L}^n$-measurable, and set $g := \mathbf{1}_E$. **Left-hand side**: for $x \in A$, $g(x) = 1$ if $x \in E$ and $0$ otherwise, so \begin{align*} \int_A \mathbf{1}_E(x) \, J_k f(x) \, d\mathcal{L}^n(x) = \int_{A \cap E} J_k f(x) \, d\mathcal{L}^n(x). \end{align*} The set $A \cap E$ is $\mathcal{L}^n$-measurable as the intersection of two $\mathcal{L}^n$-measurable sets. Apply the [Coarea Formula](/theorems/3078) to $A \cap E$. The hypotheses of Theorem 3078 are satisfied: $f: \mathbb{R}^n \to \mathbb{R}^k$ is Lipschitz with $n \ge k \ge 1$, and $A \cap E \subseteq \mathbb{R}^n$ is $\mathcal{L}^n$-measurable. The coarea formula gives \begin{align*} \int_{A \cap E} J_k f(x) \, d\mathcal{L}^n(x) = \int_{\mathbb{R}^k} \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E) \, d\mathcal{L}^k(t). \end{align*} **Right-hand side**: for each $t \in \mathbb{R}^k$, the inner integral is \begin{align*} \int_{f^{-1}(t) \cap A} \mathbf{1}_E(x) \, d\mathcal{H}^{n-k}(x) = \mathcal{H}^{n-k}(\{x \in f^{-1}(t) \cap A : x \in E\}) = \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E). \end{align*} Hence \begin{align*} \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} \mathbf{1}_E \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t) = \int_{\mathbb{R}^k} \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E) \, d\mathcal{L}^k(t). \end{align*} The two sides agree (both equal the right-hand side of Theorem 3078 applied to $A \cap E$). The $\mathcal{L}^k$-measurability of $t \mapsto \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E)$, needed to interpret the integral, is part of the conclusion of Theorem 3078 (the basic coarea formula implicitly uses this measurability). [/step]

[step:Extend to non-negative simple functions by linearity] A non-negative simple $\mathcal{L}^n$-measurable function on $\mathbb{R}^n$ has the form \begin{align*} g = \sum_{i=1}^N c_i \mathbf{1}_{E_i} \end{align*} for finitely many constants $c_i \ge 0$ and $\mathcal{L}^n$-measurable sets $E_i \subseteq \mathbb{R}^n$. By linearity of the Lebesgue integral on the left side (a finite linear combination), Step 1 applied to each $\mathbf{1}_{E_i}$: \begin{align*} \int_A g(x) J_k f(x) \, d\mathcal{L}^n(x) &= \sum_{i=1}^N c_i \int_A \mathbf{1}_{E_i}(x) J_k f(x) \, d\mathcal{L}^n(x) \\ &= \sum_{i=1}^N c_i \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} \mathbf{1}_{E_i} \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t) \\ &= \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} \sum_{i=1}^N c_i \mathbf{1}_{E_i} \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t) \\ &= \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k} \, d\mathcal{L}^k(t). \end{align*} The interchange of finite sum and integral (on both the inner $\mathcal{H}^{n-k}$-integral and the outer $\mathcal{L}^k$-integral) is justified because the sum has finitely many terms and each integrand is non-negative. The $\mathcal{L}^k$-measurability of $t \mapsto \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k} = \sum_i c_i \mathcal{H}^{n-k}(f^{-1}(t) \cap A \cap E_i)$ follows from the measurability obtained in Step 1 for each $E_i$, combined with finite linear combinations preserving measurability. [/step]

[step:Extend to general non-negative measurable $g$ by monotone convergence] Let $g: \mathbb{R}^n \to [0, +\infty]$ be $\mathcal{L}^n$-measurable. By the standard approximation theorem for non-negative measurable functions, there exists an increasing sequence $(g_j)_{j=1}^\infty$ of non-negative simple $\mathcal{L}^n$-measurable functions $g_j: \mathbb{R}^n \to [0, +\infty)$ with $g_j(x) \uparrow g(x)$ for every $x \in \mathbb{R}^n$ as $j \to \infty$. **Left-hand side limit**: since $g_j \uparrow g$ pointwise and $J_k f \ge 0$, we have $g_j J_k f \uparrow g J_k f$ pointwise on $A$. Applying the Monotone Convergence Theorem on $(A, \mathcal{L}^n \lfloor A)$, \begin{align*} \int_A g_j(x) J_k f(x) \, d\mathcal{L}^n(x) \uparrow \int_A g(x) J_k f(x) \, d\mathcal{L}^n(x) \qquad (j \to \infty). \end{align*} **Right-hand side limit**: for each fixed $t \in \mathbb{R}^k$, $g_j \uparrow g$ pointwise on $f^{-1}(t) \cap A$. Applying the Monotone Convergence Theorem on $(f^{-1}(t) \cap A, \mathcal{H}^{n-k})$: \begin{align*} \int_{f^{-1}(t) \cap A} g_j \, d\mathcal{H}^{n-k} \uparrow \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k} \qquad (j \to \infty). \end{align*} Define \begin{align*} \Psi_j: \mathbb{R}^k &\to [0, \infty] \\ t &\mapsto \int_{f^{-1}(t) \cap A} g_j \, d\mathcal{H}^{n-k}, \\ \Psi: \mathbb{R}^k &\to [0, \infty] \\ t &\mapsto \int_{f^{-1}(t) \cap A} g \, d\mathcal{H}^{n-k}. \end{align*} Each $\Psi_j$ is $\mathcal{L}^k$-measurable by Step 2. The pointwise monotone limit $\Psi_j \uparrow \Psi$ ensures $\Psi$ is $\mathcal{L}^k$-measurable as the pointwise limit of measurable functions. Applying the Monotone Convergence Theorem to $(\Psi_j)$ on $(\mathbb{R}^k, \mathcal{L}^k)$: \begin{align*} \int_{\mathbb{R}^k} \Psi_j(t) \, d\mathcal{L}^k(t) \uparrow \int_{\mathbb{R}^k} \Psi(t) \, d\mathcal{L}^k(t) \qquad (j \to \infty). \end{align*} **Combining**: by Step 2, for each $j$, \begin{align*} \int_A g_j J_k f \, d\mathcal{L}^n = \int_{\mathbb{R}^k} \Psi_j(t) \, d\mathcal{L}^k(t). \end{align*} Passing $j \to \infty$ in this equality and using the two monotone convergence statements: \begin{align*} \int_A g(x) J_k f(x) \, d\mathcal{L}^n(x) = \int_{\mathbb{R}^k} \int_{f^{-1}(t) \cap A} g(x) \, d\mathcal{H}^{n-k}(x) \, d\mathcal{L}^k(t). \end{align*} This is the coarea change of variables formula for general non-negative measurable $g$, completing the proof. [/step]