awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
⊢ Eq.{u_2 + 1} (α := F) ((fun (y : ℝ) ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x)
    ((Ioo 0 r).indicator (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) x)
have pos : ∀ (hxr : x < r),
  Eq.{u_2 + 1} (α := F) ((fun (y : ℝ) ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x)
    ((Ioo 0 r).indicator (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) x)
Tactic: by_cases hxr : x < r
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
pos :
  ∀ (hxr : x < r),
    Eq.{u_2 + 1} (α := F) ((fun (y : ℝ) ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x)
      ((Ioo 0 r).indicator (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) x)
⊢ Eq.{u_2 + 1} (α := F) ((fun (y : ℝ) ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x)
    ((Ioo 0 r).indicator (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) x)
have neg : ∀ (hxr : ¬x < r),
  Eq.{u_2 + 1} (α := F) ((fun (y : ℝ) ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x)
    ((Ioo 0 r).indicator (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) x)
Tactic: by_cases hxr : x < r
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume ↔
    @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) volume
have rw : support.{0, u_2} (M := F) ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) ⊆ Ioi 0
Tactic: rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : x ∈ support.{0, u_2} (M := F) ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x
have hx₁ : (0 < x ∧ x < r) ∧ (x = 0 → dim E - 1 = 0) ∧ ¬f x = 0
Tactic: simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      volume ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      (Ioo 0 r) volume
have rw : @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
    volume ↔
  @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
    volume
Tactic: rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
rw :
  @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      volume ↔
    @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) volume
⊢ @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      volume ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      (Ioo 0 r) volume
have rw₁ : IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
    ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) univ volume ↔
  IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
    ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) univ volume
Tactic: rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      (Ioo 0 r) volume
have _ : IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ
Tactic: calc
    _ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ := by
      rw [← integrable_indicator_iff measurableSet_ball]
      apply integrable_congr
      filter_upwards with x
      simp [indicator]
    _ ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioi 0) := by
      rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
      intro x (hx : 0 < x)
      by_cases hxr : x < r <;> simp [hxr, hx]
    _ ↔ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) := by
      rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1
    _ ↔ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioo 0 r) volume := by
      rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
_ :
  IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ
⊢ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      (Ioo 0 r) volume
have _₁ : Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ ↔
  IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
    ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume
Tactic: calc
    _ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ := by
      rw [← integrable_indicator_iff measurableSet_ball]
      apply integrable_congr
      filter_upwards with x
      simp [indicator]
    _ ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioi 0) := by
      rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
      intro x (hx : 0 < x)
      by_cases hxr : x < r <;> simp [hxr, hx]
    _ ↔ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) := by
      rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1
    _ ↔ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioo 0 r) volume := by
      rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
_ :
  IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ
_₁ :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume
⊢ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      (Ioo 0 r) volume
have _₂ : IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
    ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume ↔
  @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
    volume
Tactic: calc
    _ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ := by
      rw [← integrable_indicator_iff measurableSet_ball]
      apply integrable_congr
      filter_upwards with x
      simp [indicator]
    _ ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioi 0) := by
      rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
      intro x (hx : 0 < x)
      by_cases hxr : x < r <;> simp [hxr, hx]
    _ ↔ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) := by
      rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1
    _ ↔ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioo 0 r) volume := by
      rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
_ :
  IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ
_₁ :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume
_₂ :
  IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume ↔
    @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace
      ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) volume
⊢ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ f ‖x‖) (ball 0 r) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
      (Ioo 0 r) volume
have _₃ : @Integrable.{u_2, 0} F _ _ _ MeasureSpace.toMeasurableSpace ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y)
    volume ↔
  IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioo 0 r)
    volume
Tactic: calc
    _ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ := by
      rw [← integrable_indicator_iff measurableSet_ball]
      apply integrable_congr
      filter_upwards with x
      simp [indicator]
    _ ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioi 0) := by
      rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
      intro x (hx : 0 < x)
      by_cases hxr : x < r <;> simp [hxr, hx]
    _ ↔ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) := by
      rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1
    _ ↔ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioo 0 r) volume := by
      rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ)
      fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
have rw : Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ) (∫ (x : E) in {0}ᶜ, f ‖x‖ ∂μ)
Tactic: rw [integral_subtype_comap (measurableSet_singleton _).compl fun x ↦ f (‖x‖),
        restrict_compl_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
rw : Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ) (∫ (x : E) in {0}ᶜ, f ‖x‖ ∂μ)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ)
      fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
have rw₁ : Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ) (∫ (x : E), f ‖x‖ ∂μ)
Tactic: rw [integral_subtype_comap (measurableSet_singleton _).compl fun x ↦ f (‖x‖),
        restrict_compl_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
⊢ HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
      (∫ (x : (↑(Ioi 0) : Type)), f (↑x : ℝ) ∂Measure.volumeIoiPow (dim E - 1)) =
    dim E •
      HSMul.hSMul (β := F) (μ.real (ball 0 1))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
          y ^ (dim E - 1) • f y)
have simp : HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x))
      (Measure.withDensity
        (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume)
        fun (r : (↑(Ioi 0) : Type)) ↦ (↑((↑r : ℝ) ^ (dim E - 1)).toNNReal : ℝ≥0∞))
      fun (x : (↑(Ioi 0) : Type)) ↦ f (↑x : ℝ)) =
  dim E •
    HSMul.hSMul (β := F) (μ.real (ball 0 1))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
        y ^ (dim E - 1) • f y)
Tactic: simp only [Measure.volumeIoiPow, ENNReal.ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
⊢ HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x))
        (Measure.withDensity
          (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume)
          fun (r : (↑(Ioi 0) : Type)) ↦ (↑((↑r : ℝ) ^ (dim E - 1)).toNNReal : ℝ≥0∞))
        fun (x : (↑(Ioi 0) : Type)) ↦ f (↑x : ℝ)) =
    dim E •
      HSMul.hSMul (β := F) (μ.real (ball 0 1))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
          y ^ (dim E - 1) • f y)
have rw : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x
Tactic: rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ,
        ← 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 ↦ ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
rw : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x
⊢ HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x))
        (Measure.withDensity
          (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume)
          fun (r : (↑(Ioi 0) : Type)) ↦ (↑((↑r : ℝ) ^ (dim E - 1)).toNNReal : ℝ≥0∞))
        fun (x : (↑(Ioi 0) : Type)) ↦ f (↑x : ℝ)) =
    dim E •
      HSMul.hSMul (β := F) (μ.real (ball 0 1))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
          y ^ (dim E - 1) • f y)
have f_meas : Measurable (β := ℝ≥0) fun (r : (↑(Ioi 0) : Type)) ↦ ((↑r : ℝ) ^ (dim E - 1)).toNNReal
Tactic: rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ,
        ← 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 ↦ ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x
have rw : (↑(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 _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : (↑(x ^ (dim E - 1)).toNNReal : ℝ) • f x = x ^ (dim E - 1) • f x
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x
have rw₁ : x ^ (dim E - 1) • f x = x ^ (dim E - 1) • f x
Tactic: rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hx.out.le _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
have inl : IsEmpty ι → piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
inl : IsEmpty ι → piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
have inr : Nonempty ι → piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Nonempty ι
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
have inr : ∀ (h : Set.pi (α := α) univ s = ∅),
  piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
Tactic: rcases (pi univ s).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Nonempty ι
inr :
  ∀ (h : Set.pi (α := α) univ s = ∅),
    piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
have inr₁ : ∀ (h : (Set.pi (α := α) univ s).Nonempty),
  piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
Tactic: rcases (pi univ s).eq_empty_or_nonempty with h | h