awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
⊢ MeasurableSet (α := E) {0}ᶜ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)
rw₂ : Ne (α := Measure (↑(sphere 0 1) : Type u_1)) μ.toSphere 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

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]

Premises used: MeasureTheory.restrict_compl_singleton, MeasureTheory.integrable_congr, MeasureTheory.integrable_withDensity_iff_integrable_smul', MeasureTheory.IntegrableOn, MeasureTheory.integrableOn_iff_comap_subtypeVal, Function.comp_def, MeasureTheory.Measure.volumeIoiPow, MeasureTheory.Integrable.comp_snd_iff, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 : ℝ)

Tactic:
.of_forall ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
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)
⊢ 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:
refine .of_forall ?_
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
x : ℝ
hx : 0 < x
⊢ Eq.{u_2 + 1} (α := F)
    ((fun (x : (↑(Ioi 0) : Type)) ↦ (ENNReal.ofReal ((↑x : ℝ) ^ (dim E - 1))).toReal • f (↑x : ℝ))
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx))
    ((fun (x : (↑(Ioi 0) : Type)) ↦ (↑x : ℝ) ^ (dim E - 1) • f (↑x : ℝ))
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) x hx))

Tactic:
simp (disch := positivity) [ENNReal.toReal_ofReal]

Premises used: ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
⊢ Measurable (β := ℝ≥0∞) fun (r : (↑(Ioi 0) : Type)) ↦ ENNReal.ofReal ((↑r : ℝ) ^ (dim E - 1))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
⊢ ∀ᵐ (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:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
⊢ MeasurableSet (α := ℝ) (Ioi 0)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))
⊢ Ne (α := Measure (↑(sphere 0 1) : Type u_1)) μ.toSphere 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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, 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‖) μ
⊢ 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:
rw [← integrable_indicator_iff measurableSet_ball]

Premises used: measurableSet_ball, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 : ℝ
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‖
⊢ 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:
apply integrable_congr

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 : ℝ
h : ∀ (x : E), indicator (ball 0 r) (fun (x : E) ↦ f ‖x‖) x = (Iio r).indicator f ‖x‖
⊢ 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:
filter_upwards with x
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 : E
⊢ indicator (ball 0 r) (fun (x : E) ↦ f ‖x‖) x = (Iio r).indicator f ‖x‖

Tactic:
simp [indicator]

Premises used: Set.indicator
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 :
  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)
⊢ 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:
rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_Ioi, MeasureTheory.integrable_fun_norm_addHaar
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 : ℝ
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)
⊢ 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)

Tactic:
(hx : 0 < x)
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
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:
simp [hxr, hx]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
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:
simp [hxr, hx]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 : support.{0, u_2} (M := F) ((Ioo 0 r).indicator fun (y : ℝ) ↦ y ^ (dim E - 1) • f y) ⊆ Ioi 0
⊢ 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:
rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)
⊢ (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

Premises used: Set.mem_Ioo, Set.support_indicator, Set.mem_inter_iff, pow_eq_zero_iff', ne_eq, not_or, Function.mem_support, Decidable.not_not, not_and, smul_eq_zero
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 ∧ x < r) ∧ (x = 0 → dim E - 1 = 0) ∧ ¬f x = 0
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x

Tactic:
mem_Ioi.mpr hx.1.1

Premises used: Iff.mpr, Set.mem_Ioi, And.left
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 ∧ x < r) ∧ (x = 0 → dim E - 1 = 0) ∧ ¬f x = 0
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x

Tactic:
refine mem_Ioi.mpr hx.1.1

Premises used: Iff.mpr, Set.mem_Ioi, And.left
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
rw₁ 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
⊢ @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:
rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]

Premises used: measurableSet_Ioo, MeasureTheory.integrableOn_univ, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
_₃ :
  @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
⊢ 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

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]

Premises used: Norm.norm, Real, Set.Ioi, Set.indicator, HSub.hSub, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, HPow.hPow, MeasureTheory.MeasureSpace.volume, HSMul.hSMul, OfNat.ofNat, Set.Iio, Set.Ioo, Module.finrank