Polar coordinates for lintegrals in Mathlib: ∫⁻ g dμ = ∫⁻ θ ∈ sphere, ∫⁻ r>0, r^(n-1) g(r•θ)

Mathlib has the measure-level statement (Measure.measurePreserving_homeomorphUnitSphereProd μ : MeasurePreserving (homeomorphUnitSphereProd E) (μ.comap (↑)) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))) but no ready lintegral formula. Proof chain that compiled first try modulo small fixes: (1) rw [restrict_compl_singleton] (it's MeasureTheory.restrict_compl_singleton, not Measure.; needs NoAtoms, ok for Haar + Nontrivial E) to pass to {0}ᶜ; (2) (lintegral_subtype_comap (measurableSet_singleton 0).compl g).symm to the subtype with μ.comap (↑); (3) with e := (homeomorphUnitSphereProd E).toMeasurableEquiv, ((hmp.symm e).lintegral_comp_emb e.symm.measurableEmbedding fun x ↦ g x).symm; then rfl turns g (e.symm y) into g (y.2 • y.1); (4) lintegral_prod _ hgm.aemeasurable; (5) per θ: rw [Measure.volumeIoiPow, lintegral_withDensity_eq_lintegral_mul _ hd hgθ] then lintegral_subtype_comap measurableSet_Ioi. Gotcha in (5): give hd/hgθ as have with the explicit lambda type (fun r : Ioi (0:ℝ) ↦ ...); passing hg.comp ... makes the rewrite pattern a composition g ∘ _ and rw fails. Also parenthesize the inner integral in statements: ∫⁻ θ, (∫⁻ r in Ioi 0, ...) ∂μ.toSphere, otherwise ∂μ.toSphere binds to the inner set integral. Application: vol of Ball's body K_n(f) = (1/n)∫f.