-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
lemma integral_fun_norm_addHaar (f : ℝ → F) :
    ∫ x, f (‖x‖) ∂μ = dim E • (μ (ball 0 1)).toReal • ∫ y in Ioi (0 : ℝ), y ^ (dim E - 1) • f y :=
  calc
    ∫ x, f (‖x‖) ∂μ = ∫ x : ({(0)}ᶜ : Set E), f (‖x.1‖) ∂(μ.comap (↑))

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ (μ.toSphere univ).toReal • ∫ (x : ↑(Ioi 0)), f ↑x ∂Measure.volumeIoiPow (dim E - 1) =
    dim E • (μ (ball 0 1)).toReal • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Tactic:
simp only [Measure.volumeIoiPow, ENNReal.ofReal]

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ ((μ.toSphere univ).toReal •
      ∫ (x : ↑(Ioi 0)), f ↑x ∂(Measure.comap Subtype.val volume).withDensity fun r => ↑(↑r ^ (dim E - 1)).toNNReal) =
    dim E • (μ (ball 0 1)).toReal • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Proof state:
case f_meas
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable fun r => (↑r ^ (dim E - 1)).toNNReal

Tactic:
exact (measurable_subtype_coe.pow_const _).real_toNNReal

Result:
no goals

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ ∫ (x : E), f ‖x‖ ∂μ = ∫ (x : ↑{0}ᶜ), f ‖↑x‖ ∂Measure.comap Subtype.val μ

Tactic:
rw [integral_subtype_comap (measurableSet_singleton _).compl fun x ↦ f (‖x‖),
  restrict_compl_singleton]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ ((μ.toSphere univ).toReal •
      ∫ (x : ↑(Ioi 0)), f ↑x ∂(Measure.comap Subtype.val volume).withDensity fun r => ↑(↑r ^ (dim E - 1)).toNNReal) =
    dim E • (μ (ball 0 1)).toReal • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Tactic:
rw [integral_withDensity_eq_integral_smul, μ.toSphere_apply_univ,
  ENNReal.toReal_mul, ENNReal.toReal_natCast, ← nsmul_eq_mul, smul_assoc,
  integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,
  setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ ?_]

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x

case f_meas
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable fun r => (↑r ^ (dim E - 1)).toNNReal

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x

Tactic:
rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hx.out.le _)]

Result:
no goals