[proofplan] The level-set formula is the case $k = 1$ of the [Coarea Change of Variables](/theorems/3079) applied with weight $h := g / |\nabla f|$ on the regular set $R := \{|\nabla f| > 0\}$ and $h := 0$ on the critical set $C := \{|\nabla f| = 0\}$. Step 1 identifies the coarea factor $J_1 f$ with $|\nabla f|$ for scalar Lipschitz maps. Step 2 applies Theorem 3079 to $h$, producing the LHS as $\int_R g \, d\mathcal{L}^n$ on the left and the desired iterated integral on the right (with the convention boundary on $C$). Step 3 uses the [Coarea Formula](/theorems/3078) with weight $\mathbf{1}_C$ to show $\mathcal{H}^{n-1}(f^{-1}(t) \cap C) = 0$ for $\mathcal{L}^1$-a.e. $t$, so the convention on $C$ alters the inner integral only on $\mathcal{H}^{n-1}$-null subsets and the RHS is well-defined. [/proofplan] [step:Identify the coarea factor $J_1 f$ with $|\nabla f|$ for the scalar Lipschitz map $f$] By [Rademacher's Theorem](/theorems/3069), the Lipschitz map $f: \mathbb{R}^n \to \mathbb{R}$ is differentiable at $\mathcal{L}^n$-a.e. $x \in \mathbb{R}^n$. We identify $\nabla f(x) \in \mathbb{R}^n$ with a column vector; correspondingly, the Jacobian matrix at a point of differentiability is the row vector \begin{align*} Jf_x = (\nabla f(x))^\top \in \mathbb{R}^{1 \times n}. \end{align*} Since $n \ge 1 = k$, the $1$-dimensional Jacobian (the coarea factor) is \begin{align*} J_1 f(x) = \sqrt{\det\!\bigl(Jf_x \, (Jf_x)^\top\bigr)} = \sqrt{(\nabla f(x))^\top \nabla f(x)} = |\nabla f(x)|, \end{align*} where the inner product $Jf_x \, (Jf_x)^\top \in \mathbb{R}^{1 \times 1}$ equals $\sum_{i=1}^n (\partial_{x_i} f(x))^2 = |\nabla f(x)|^2$. Hence $J_1 f(x) = |\nabla f(x)|$ at $\mathcal{L}^n$-a.e. $x \in \mathbb{R}^n$. Extend $\nabla f$ by $0$ on the (Lebesgue null) non-differentiability set so that $\nabla f$ — and hence $|\nabla f|$ and $J_1 f$ — are defined everywhere on $\mathbb{R}^n$ as $\mathcal{L}^n$-measurable functions. [/step] [step:Apply Coarea Change of Variables to the weight $h = g/|\nabla f|$ on the regular set] Define the regular and critical sets \begin{align*} R &:= \{x \in \mathbb{R}^n : |\nabla f(x)| > 0\}, \\ C &:= \{x \in \mathbb{R}^n : |\nabla f(x)| = 0\} = \mathbb{R}^n \setminus R. \end{align*} Both $R$ and $C$ are Borel sets because $|\nabla f|: \mathbb{R}^n \to [0, +\infty)$ is Borel measurable (as established in Step 1). Define the weight \begin{align*} h: \mathbb{R}^n &\to [0, +\infty] \\ x &\mapsto \begin{cases} g(x)/|\nabla f(x)| & \text{if } x \in R, \\ 0 & \text{if } x \in C. \end{cases} \end{align*} We verify $h$ is $\mathcal{L}^n$-measurable: on the Borel set $R$, $h = g \cdot (1/|\nabla f|)$ is measurable as the product of the measurable function $g$ and the measurable function $1/|\nabla f|$ (the reciprocal of a positive measurable function); on the Borel set $C$, $h \equiv 0$. Gluing these on the disjoint union $R \sqcup C = \mathbb{R}^n$ gives a measurable $h$. Non-negativity $h \ge 0$ follows from $g \ge 0$ and $|\nabla f| > 0$ on $R$. We now invoke the [Coarea Change of Variables](/theorems/3079) with parameters $A := \mathbb{R}^n$, $k := 1$, ambient dimension $n \ge 1$, the Lipschitz map $f: \mathbb{R}^n \to \mathbb{R}$, and the weight $h$. The hypotheses of Theorem 3079 are: (i) $f$ Lipschitz from $\mathbb{R}^n$ to $\mathbb{R}^k$ with $n \ge k$ — verified, $k = 1$, $n \ge 1$; (ii) $A \subseteq \mathbb{R}^n$ is $\mathcal{L}^n$-measurable — verified, $A = \mathbb{R}^n$; (iii) $h: A \to [0, +\infty]$ is $\mathcal{L}^n$-measurable — verified above. Theorem 3079 yields \begin{align*} \int_{\mathbb{R}^n} h(x) \, J_1 f(x) \, d\mathcal{L}^n(x) = \int_{-\infty}^{\infty} \int_{f^{-1}(t)} h(x) \, d\mathcal{H}^{n-1}(x) \, d\mathcal{L}^1(t), \end{align*} together with $\mathcal{L}^1$-measurability of the inner integral $t \mapsto \int_{f^{-1}(t)} h \, d\mathcal{H}^{n-1}$. We compute each side. For the left side, partition $\mathbb{R}^n = R \sqcup C$: \begin{align*} \int_{\mathbb{R}^n} h \cdot J_1 f \, d\mathcal{L}^n &= \int_R h \cdot J_1 f \, d\mathcal{L}^n + \int_C h \cdot J_1 f \, d\mathcal{L}^n. \end{align*} By the definition of $h$, the integrand vanishes on $C$, so the second integral is $0$. On $R$, by Step 1 we have $J_1 f = |\nabla f|$ at $\mathcal{L}^n$-a.e. point, so \begin{align*} h(x) \, J_1 f(x) = \frac{g(x)}{|\nabla f(x)|} \cdot |\nabla f(x)| = g(x) \qquad \text{for } \mathcal{L}^n\text{-a.e. } x \in R. \end{align*} Therefore the left side equals $\int_R g \, d\mathcal{L}^n$, which is precisely $\int_{\{|\nabla f| > 0\}} g \, d\mathcal{L}^n$. For the right side, the inner integrand is $h(x)$, which on the level set $f^{-1}(t)$ takes the value $g(x)/|\nabla f(x)|$ at points in $R$ and $0$ at points in $C$, in accordance with the convention adopted in the theorem statement. So the right side is exactly \begin{align*} \int_{-\infty}^{\infty} \int_{f^{-1}(t)} \frac{g(x)}{|\nabla f(x)|} \, d\mathcal{H}^{n-1}(x) \, d\mathcal{L}^1(t), \end{align*} provided that this expression is well-defined, i.e., that the convention $g/|\nabla f| = 0$ on $C$ does not introduce ambiguity. We address this in Step 3. [/step] [step:Verify that the convention on $C$ does not affect the inner integral on a.e. level set] We now confirm that the right-hand side as written in the theorem, \begin{align*} \int_{-\infty}^{\infty} \int_{f^{-1}(t)} \frac{g(x)}{|\nabla f(x)|} \, d\mathcal{H}^{n-1}(x) \, d\mathcal{L}^1(t), \end{align*} is well-defined under the convention $g/|\nabla f| := 0$ on $C$. The concern is that on a given level set $f^{-1}(t)$, points lying in $C$ have $g/|\nabla f|$ formally undefined; the convention assigns the value $0$ to such points, but this could change the value of the inner integral. We show this concern is illusory for $\mathcal{L}^1$-a.e. $t$. Apply the [Coarea Formula](/theorems/3078) with $k = 1$, ambient dimension $n$, the Lipschitz map $f: \mathbb{R}^n \to \mathbb{R}$, and weight $\mathbf{1}_C$ (the indicator of $C$, which is Borel measurable since $C$ is Borel). Theorem 3078 gives \begin{align*} \int_{\mathbb{R}^n} \mathbf{1}_C(x) \, J_1 f(x) \, d\mathcal{L}^n(x) = \int_{-\infty}^{\infty} \mathcal{H}^{n-1}(f^{-1}(t) \cap C) \, d\mathcal{L}^1(t). \end{align*} The left side equals $\int_C |\nabla f| \, d\mathcal{L}^n$ (using $J_1 f = |\nabla f|$ a.e. from Step 1), and $|\nabla f| = 0$ on $C$, hence $\int_C |\nabla f| \, d\mathcal{L}^n = 0$. Thus \begin{align*} \int_{-\infty}^{\infty} \mathcal{H}^{n-1}(f^{-1}(t) \cap C) \, d\mathcal{L}^1(t) = 0. \end{align*} The integrand is non-negative, so \begin{align*} \mathcal{H}^{n-1}(f^{-1}(t) \cap C) = 0 \qquad \text{for } \mathcal{L}^1\text{-a.e. } t \in \mathbb{R}. \end{align*} Consequently, for $\mathcal{L}^1$-a.e. $t$, the level set $f^{-1}(t)$ decomposes as \begin{align*} f^{-1}(t) = (f^{-1}(t) \cap R) \sqcup (f^{-1}(t) \cap C), \end{align*} with the second piece $\mathcal{H}^{n-1}$-null. Hence for $\mathcal{L}^1$-a.e. $t$, \begin{align*} \int_{f^{-1}(t)} h \, d\mathcal{H}^{n-1} = \int_{f^{-1}(t) \cap R} h \, d\mathcal{H}^{n-1} = \int_{f^{-1}(t) \cap R} \frac{g}{|\nabla f|} \, d\mathcal{H}^{n-1} = \int_{f^{-1}(t)} \frac{g(x)}{|\nabla f(x)|} \, d\mathcal{H}^{n-1}(x), \end{align*} where in the final step we extend the integration domain back to all of $f^{-1}(t)$ — this leaves the integral unchanged since the discarded set $f^{-1}(t) \cap C$ is $\mathcal{H}^{n-1}$-null and the integrand on $f^{-1}(t) \cap C$ is set to $0$ by convention (so the convention boundary is operationally invisible). The right-hand side of the identity from Step 2 therefore equals the right-hand side of the theorem statement, and combining with Step 2 yields \begin{align*} \int_{\{|\nabla f| > 0\}} g(x) \, d\mathcal{L}^n(x) = \int_{-\infty}^{\infty} \int_{f^{-1}(t)} \frac{g(x)}{|\nabla f(x)|} \, d\mathcal{H}^{n-1}(x) \, d\mathcal{L}^1(t), \end{align*} as claimed. The $\mathcal{L}^1$-measurability of the inner integral is delivered by Theorem 3079. [/step]