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
s : Set (↑(sphere 0 1) : Type u_1)
r : (↑(Ioi 0) : Type)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (image (α := (↑{0}ᶜ : Type u_1)) (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
          ((⇑(homeomorphUnitSphereProd E) :
              (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ⁻¹'
            s ×ˢ Iio r)) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (Ioo 0 (↑r : ℝ) • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s) :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      ((fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦
          (↑((Homeomorph.symm (homeomorphUnitSphereProd E) :
                  (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
                x) :
            E)) ''
        s ×ˢ Iio r) :
    ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      ((fun (x : (↑(sphere 0 1) : Type u_1) × { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }) ↦
          (↑x.2 : ℝ) • (↑x.1 : E)) ''
        s ×ˢ Iio r) :
    ℝ≥0∞)
Tactic: rw [← image2_smul, image2_image_right, ← Homeomorph.image_symm, image_image,
    ← image_subtype_val_Ioi_Iio, image2_image_left, image2_swap, ← image_prod]
-- 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
s : Set (↑(sphere 0 1) : Type u_1)
hs : MeasurableSet s
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
have rw : (HSMul.hSMul (β := Measure (↑(sphere 0 1) : Type u_1)) (dim E)
        (fst
          (restrict
            (comap
              (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                  (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
              μ)
            (SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
              (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))))) :
      (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞)
    s =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
      ℝ≥0∞)
Tactic: rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
    ((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
      (Homeomorph.measurableEmbedding _)).comap_apply,
    image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]
-- 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
s : Set (↑(sphere 0 1) : Type u_1)
hs : MeasurableSet s
rw :
  (HSMul.hSMul (β := Measure (↑(sphere 0 1) : Type u_1)) (dim E)
          (fst
            (restrict
              (comap
                (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                  (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                  (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                    (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
                μ)
              (SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))))) :
        (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞)
      s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
have rw₁ : HSMul.hSMul (β := ℝ≥0∞) (dim E)
    (((fst
              (restrict
                (comap
                  (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                    (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                      (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
                  μ)
                (SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                  (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1)))) :
            Measure (↑(sphere 0 1) : Type u_1)) :
          (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞)
        s :
      ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
      ℝ≥0∞)
Tactic: rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
    ((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
      (Homeomorph.measurableEmbedding _)).comap_apply,
    image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]
-- 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
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (ball 0 (HMul.hMul (α := ℝ) 1 1) \ closedBall 0 (HMul.hMul (α := ℝ) 0 1)) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
Tactic: rw [μ.toSphere_apply' .univ, image_univ, Subtype.range_coe, Ioo_smul_sphere_zero]
-- 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
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 (HMul.hMul (α := ℝ) 1 1) \ closedBall 0 (HMul.hMul (α := ℝ) 0 1)) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
have ha : LE.le (α := ℝ) 0 0
Tactic: rw [μ.toSphere_apply' .univ, image_univ, Subtype.range_coe, Ioo_smul_sphere_zero]
-- 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
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 (HMul.hMul (α := ℝ) 1 1) \ closedBall 0 (HMul.hMul (α := ℝ) 0 1)) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
ha : LE.le (α := ℝ) 0 0
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
have hr : LT.lt (α := ℝ) 0 1
Tactic: rw [μ.toSphere_apply' .univ, image_univ, Subtype.range_coe, Ioo_smul_sphere_zero]
-- 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 : μ.IsOpenPosMeasure
⊢ ∀ (U : Set (↑(sphere 0 1) : Type u_1)),
    IsOpen U →
      U.Nonempty →
        Ne (α := ℝ≥0∞)
          (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) U : ℝ≥0∞)
          (0 : ℝ≥0∞)
have a : Nontrivial E
Tactic: nontriviality E using not_nonempty_iff_eq_empty
-- 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 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
⊢ Ne (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) U : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
      ℝ≥0∞) ≠
  0
Tactic: rw [μ.toSphere_apply' hUo.measurableSet]
-- 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 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
        ℝ≥0∞) ≠
    0
have apply : Ne (α := ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: apply mul_ne_zero (by simp [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
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have a : Nontrivial E
Tactic: nontriviality E
-- 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 : Nontrivial E
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: rw [toSphere_apply_univ', measure_diff_null (measure_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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
h : Nontrivial E
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥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∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: rw [toSphere_apply_univ', measure_diff_null (measure_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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
⊢ Eq (α := Measure (↑(sphere 0 1) : Type u_1)) μ.toSphere 0 ↔ dim E = 0
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) = 0 ↔
  dim E = 0
Tactic: rw [← measure_univ_eq_zero, toSphere_apply_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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
⊢ LT.lt (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) < ∞
Tactic: rw [toSphere_apply_univ']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
⊢ (volumeIoiPow n : (a : Set (↑(Ioi 0) : Type)) → ℝ≥0∞) (Iio x) =
    ENNReal.ofReal ((↑x : ℝ) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hr₀ : 0 ≤ (↑x : ℝ)
Tactic: have hr₀ : 0 ≤ x.1 := le_of_lt x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
hr₀ : 0 ≤ (↑x : ℝ)
⊢ (ae (F := Measure ℝ) (restrict volume (Ioc 0 (↑x : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ x ^ n
have h : ∀ (y : ℝ) (hy : y ∈ Ioc 0 (↑x : ℝ)), 0 y ≤ y ^ n
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioc] with y hy
-- 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
⊢ MeasurePreserving (α := (↑{0}ᶜ : Type u_1)) (β := (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
    (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
    (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ)
    (Measure.prod μ.toSphere (volumeIoiPow (dim E - 1)))
have a : Nontrivial E
Tactic: nontriviality E
-- 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 : Nontrivial E
⊢ MeasurePreserving (α := (↑{0}ᶜ : Type u_1)) (β := (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
    (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
    (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ)
    (Measure.prod μ.toSphere (volumeIoiPow (dim E - 1)))
have refine : Eq (α := Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) (Measure.prod μ.toSphere (volumeIoiPow (dim E - 1)))
  (map (α := (↑{0}ᶜ : Type u_1))
    (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
    (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ))
Tactic: refine ⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩
-- 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 : Nontrivial E
⊢ Eq (α := Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)))
    (Measure.prod μ.toSphere (volumeIoiPow (dim E - 1)))
    (map (α := (↑{0}ᶜ : Type u_1))
      (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
      (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ))
have refine : ∀ (s : Set (↑(sphere 0 1) : Type u_1))
  (hs :
    Membership.mem (γ := Set (Set (↑(sphere 0 1) : Type u_1))) {s : Set (↑(sphere 0 1) : Type u_1) | MeasurableSet s} s)
  (r : (↑(Ioi 0) : Type)),
  ((map (α := (↑{0}ᶜ : Type u_1))
            (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
            (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) :
          Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) :
        (a : Set ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) → ℝ≥0∞)
      (s ×ˢ Iio r) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s : ℝ≥0∞)
      ((volumeIoiPow (dim E - 1) : (a : Set (↑(Ioi 0) : Type)) → ℝ≥0∞) (Iio r) : ℝ≥0∞)
Tactic: refine prod_eq_generateFrom generateFrom_measurableSet
    ((borel_eq_generateFrom_Iio _).symm.trans BorelSpace.measurable_eq.symm)
    isPiSystem_measurableSet isPiSystem_Iio
    μ.toSphere.toFiniteSpanningSetsIn (finiteSpanningSetsIn_volumeIoiPow_range_Iio _)
    fun s hs ↦ forall_mem_range.2 fun r ↦ ?_
-- 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
h : Nontrivial E
s : Set (↑(sphere 0 1) : Type u_1)
hs : Membership.mem (γ := Set (Set (↑(sphere 0 1) : Type u_1))) {s : Set (↑(sphere 0 1) : Type u_1) | MeasurableSet s} s
r : (↑(Ioi 0) : Type)
⊢ ((map (α := (↑{0}ᶜ : Type u_1))
            (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
            (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) :
          Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) :
        (a : Set ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) → ℝ≥0∞)
      (s ×ˢ Iio r) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s : ℝ≥0∞)
      ((volumeIoiPow (dim E - 1) : (a : Set (↑(Ioi 0) : Type)) → ℝ≥0∞) (Iio r) : ℝ≥0∞)
have this : Ioo 0 (↑r : ℝ) = HSMul.hSMul (β := Set ℝ) (↑r : ℝ) (Ioo 0 1)
Tactic: have : Ioo (0 : ℝ) r = r.1 • Ioo (0 : ℝ) 1 := by simp [LinearOrderedField.smul_Ioo r.2.out]
-- 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
h : Nontrivial E
s : Set (↑(sphere 0 1) : Type u_1)
hs : Membership.mem (γ := Set (Set (↑(sphere 0 1) : Type u_1))) {s : Set (↑(sphere 0 1) : Type u_1) | MeasurableSet s} s
r : (↑(Ioi 0) : Type)
this : Ioo 0 (↑r : ℝ) = HSMul.hSMul (β := Set ℝ) (↑r : ℝ) (Ioo 0 1)
⊢ ((map (α := (↑{0}ᶜ : Type u_1))
            (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
            (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) :
          Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) :
        (a : Set ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) → ℝ≥0∞)
      (s ×ˢ Iio r) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s : ℝ≥0∞)
      ((volumeIoiPow (dim E - 1) : (a : Set (↑(Ioi 0) : Type)) → ℝ≥0∞) (Iio r) : ℝ≥0∞)
have hpos : 0 < dim E
Tactic: have hpos : 0 < dim E := Module.finrank_pos
-- 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 : Nontrivial E
s : Set (↑(sphere 0 1) : Type u_1)
hs : Membership.mem (γ := Set (Set (↑(sphere 0 1) : Type u_1))) {s : Set (↑(sphere 0 1) : Type u_1) | MeasurableSet s} s
r : (↑(Ioi 0) : Type)
this : Ioo 0 (↑r : ℝ) = HSMul.hSMul (β := Set ℝ) (↑r : ℝ) (Ioo 0 1)
hpos : 0 < dim E
⊢ ((map (α := (↑{0}ᶜ : Type u_1))
            (⇑(homeomorphUnitSphereProd E) : (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))
            (comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ) :
          Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) :
        (a : Set ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) → ℝ≥0∞)
      (s ×ˢ Iio r) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s : ℝ≥0∞)
      ((volumeIoiPow (dim E - 1) : (a : Set (↑(Ioi 0) : Type)) → ℝ≥0∞) (Iio r) : ℝ≥0∞)
have hb : Ne (α := ℝ) (↑(dim E) : ℝ) 0
Tactic: rw [(Homeomorph.measurableEmbedding _).map_apply, toSphere_apply' _ hs, volumeIoiPow_apply_Iio,
    comap_subtype_coe_apply (measurableSet_singleton _).compl, toSphere_apply_aux, this,
    smul_assoc, μ.addHaar_smul_of_nonneg r.2.out.le, Nat.sub_add_cancel hpos, Nat.cast_pred hpos,
    sub_add_cancel, mul_right_comm, ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, mul_div_cancel₀]