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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
this_1 : Nontrivial E
this :
  ∀ {ε : ℝ} (hε : 0 < ε) (hε₂ : ε ≤ 2),
    HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
      ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
hε₂ : ¬ε ≤ 2
⊢ LE.le (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞)
        (ball x (min ε 2)) :
      ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε) :
      ℝ≥0∞)
have h : min ε 2 ≤ ε
Tactic: gcongr
-- 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
have rw : HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball (↑x : E) ε ∩ sphere 0 1)) : ℝ≥0∞)
Tactic: rw [μ.toSphere_apply' measurableSet_ball, Subtype.image_ball, setOf_mem_eq]
-- 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball (↑x : E) ε ∩ sphere 0 1)) : ℝ≥0∞)
have grw : HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (ball ((1 - ε / 4) • (↑x : E)) (ε / 4)) : ℝ≥0∞)
Tactic: grw [← ball_subset_sector_of_small_epsilon]
-- 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
grw :
  HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball ((1 - ε / 4) • (↑x : E)) (ε / 4)) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball (↑x : E) ε ∩ sphere 0 1)) : ℝ≥0∞)
have hx : ‖(↑x : E)‖ = 1
Tactic: grw [← ball_subset_sector_of_small_epsilon]
-- 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball ((1 - ε / 4) • (↑x : E)) (ε / 4)) : ℝ≥0∞)
have hdim : dim E ≠ 0
Tactic: have hdim : Module.finrank ℝ E ≠ 0 := Module.finrank_pos.ne'
-- 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
hdim : dim E ≠ 0
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball ((1 - ε / 4) • (↑x : E)) (ε / 4)) : ℝ≥0∞)
have this₁ : min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε
Tactic: have : min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε := by simpa
-- 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
⊢ (↑(toSphereBallBound (dim E) ε) : ℝ) * μ.real (ball 0 1) ≤ Measure.real μ.toSphere (ball x ε)
have h₂ : Ne (α := ℝ≥0∞)
  (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)) ∞
Tactic: grw [Measure.real, Measure.real, ← toSphereBallBound_mul_measure_unitBall_le_toSphere_ball μ hε,
    ENNReal.toReal_mul, ENNReal.coe_toReal]
-- 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
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have this : @Integrable _ _ _ (↑{0}ᶜ : Type u_1)
    (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
    (comp (β := (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
      (f ∘ Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) ∘ Prod.snd)
      (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)))
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
  Integrable (α := (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
    (f ∘ Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) ∘ Prod.snd)
    (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
Tactic: have := μ.measurePreserving_homeomorphUnitSphereProd.integrable_comp_emb (g := f ∘ (↑) ∘ Prod.snd)
    (Homeomorph.measurableEmbedding _)
-- 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
this :
  @Integrable _ _ _ (↑{0}ᶜ : Type u_1)
      (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (comp (β := (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
        (f ∘ Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) ∘ Prod.snd)
        (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable (α := (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
      (f ∘ Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) ∘ Prod.snd)
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have this₁ : @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
    (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
  Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
    (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
Tactic: simp only [comp_def, homeomorphUnitSphereProd_apply_snd_coe] at this
Cleared hypotheses: this
-- 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
this :
  @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have rw : Filter.EventuallyEq.{0, u_2} (β := F)
  (ae (F := Measure (↑(Ioi 0) : Type))
    (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume))
  (fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
  fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)
Tactic: rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn,
    integrableOn_iff_comap_subtypeVal (by measurability), comp_def, this,
    Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),
    integrableOn_iff_comap_subtypeVal, comp_def, Measure.volumeIoiPow,
    integrable_withDensity_iff_integrable_smul', integrable_congr]
-- 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
this :
  @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
rw :
  Filter.EventuallyEq.{0, u_2} (β := F)
    (ae (F := Measure (↑(Ioi 0) : Type))
      (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume))
    (fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
    fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have hf : Measurable (β := ℝ≥0∞) fun (r : (↑(Ioi 0) : Type)) ↦ ENNReal.ofReal ((↑r : ℝ) ^ (dim E - 1))
Tactic: rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn,
    integrableOn_iff_comap_subtypeVal (by measurability), comp_def, this,
    Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),
    integrableOn_iff_comap_subtypeVal, comp_def, Measure.volumeIoiPow,
    integrable_withDensity_iff_integrable_smul', integrable_congr]
-- 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
this :
  @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
rw :
  Filter.EventuallyEq.{0, u_2} (β := F)
    (ae (F := Measure (↑(Ioi 0) : Type))
      (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume))
    (fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
    fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)
hf : Measurable (β := ℝ≥0∞) fun (r : (↑(Ioi 0) : Type)) ↦ ENNReal.ofReal ((↑r : ℝ) ^ (dim E - 1))
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have hflt : ∀ᵐ (x :
  (↑(Ioi 0) : Type)) ∂Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume,
  ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1)) < ∞
Tactic: rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn,
    integrableOn_iff_comap_subtypeVal (by measurability), comp_def, this,
    Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),
    integrableOn_iff_comap_subtypeVal, comp_def, Measure.volumeIoiPow,
    integrable_withDensity_iff_integrable_smul', integrable_congr]
-- 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
this :
  @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
rw :
  Filter.EventuallyEq.{0, u_2} (β := F)
    (ae (F := Measure (↑(Ioi 0) : Type))
      (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume))
    (fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
    fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)
hf : Measurable (β := ℝ≥0∞) fun (r : (↑(Ioi 0) : Type)) ↦ ENNReal.ofReal ((↑r : ℝ) ^ (dim E - 1))
hflt :
  ∀ᵐ (x :
    (↑(Ioi 0) : Type)) ∂Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume,
    ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1)) < ∞
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have rw₁ : MeasurableSet (α := ℝ) (Ioi 0)
Tactic: rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn,
    integrableOn_iff_comap_subtypeVal (by measurability), comp_def, this,
    Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),
    integrableOn_iff_comap_subtypeVal, comp_def, Measure.volumeIoiPow,
    integrable_withDensity_iff_integrable_smul', integrable_congr]
-- 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
this :
  @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
rw :
  Filter.EventuallyEq.{0, u_2} (β := F)
    (ae (F := Measure (↑(Ioi 0) : Type))
      (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume))
    (fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
    fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)
hf : Measurable (β := ℝ≥0∞) fun (r : (↑(Ioi 0) : Type)) ↦ ENNReal.ofReal ((↑r : ℝ) ^ (dim E - 1))
hflt :
  ∀ᵐ (x :
    (↑(Ioi 0) : Type)) ∂Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume,
    ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1)) < ∞
rw₁ : MeasurableSet (α := ℝ) (Ioi 0)
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ f ‖x‖) μ ↔
    IntegrableOn.{0, u_2} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
      volume
have rw₂ : Ne (α := Measure (↑(sphere 0 1) : Type u_1)) μ.toSphere 0
Tactic: rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn,
    integrableOn_iff_comap_subtypeVal (by measurability), comp_def, this,
    Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),
    integrableOn_iff_comap_subtypeVal, comp_def, Measure.volumeIoiPow,
    integrable_withDensity_iff_integrable_smul', integrable_congr]
-- 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
this :
  @Integrable.{u_2, u_1} F _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦ f (↑x.2 : ℝ))
      (Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))
⊢ Filter.EventuallyEq.{0, u_2} (β := F)
    (ae (F := Measure (↑(Ioi 0) : Type))
      (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume))
    (fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
    fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)
have refine : ∀ (x : (↑(Ioi 0) : Type)),
  Eq.{u_2 + 1} (α := F)
    ((fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ)) x)
    ((fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ)) x)
Tactic: refine .of_forall ?_
-- 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‖) μ
have rw : Integrable.{u_2, u_1} (ε := F) (indicator (ball 0 r) fun (x : E) ↦ f ‖x‖) μ ↔
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ
Tactic: rw [← integrable_indicator_iff measurableSet_ball]
-- 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, u_1} (ε := F) (indicator (ball 0 r) fun (x : E) ↦ f ‖x‖) μ ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (Iio r).indicator f ‖x‖) μ
have h : Filter.EventuallyEq.{u_1, u_2} (β := F) (ae μ) (indicator (ball 0 r) fun (x : E) ↦ f ‖x‖) fun (x : E) ↦
  (Iio r).indicator f ‖x‖
Tactic: apply integrable_congr
-- 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 : ℝ
⊢ Filter.EventuallyEq.{u_1, u_2} (β := F) (ae μ) (indicator (ball 0 r) fun (x : E) ↦ f ‖x‖) fun (x : E) ↦
    (Iio r).indicator f ‖x‖
have h : ∀ (x : E), indicator (ball 0 r) (fun (x : E) ↦ f ‖x‖) x = (Iio r).indicator f ‖x‖
Tactic: filter_upwards with x
-- 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, 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
have rw : EqOn.{0, u_2} (β := F) (fun (y : ℝ) ↦ y ^ (dim E - 1) • (Iio r).indicator f y)
  ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) (Ioi 0)
Tactic: rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
-- 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 : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 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 this : ∀ (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)
Tactic: (hx : 0 < x)