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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) = 0 ↔
    dim E = 0

Tactic:
simp [IsOpen.measure_ne_zero]

Premises used: IsOpen.measure_ne_zero
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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 ↔ Subsingleton E

Tactic:
μ.toSphere_eq_zero_iff_finrank.trans Module.finrank_zero_iff

Premises used: Iff.trans, MeasureTheory.Measure.toSphere_eq_zero_iff_finrank, Module.finrank_zero_iff
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
inst_6 : Nontrivial E
⊢ Ne (α := Measure (↑(sphere 0 1) : Type u_1)) μ.toSphere 0

Tactic:
simp [toSphere_eq_zero_iff, not_subsingleton]

Premises used: not_subsingleton, MeasureTheory.Measure.toSphere_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [toSphere_apply_univ']

Premises used: MeasureTheory.Measure.toSphere_apply_univ'
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) < ∞

Tactic:
ENNReal.mul_lt_top (ENNReal.natCast_lt_top _) <|
      measure_ball_lt_top.trans_le' <| measure_mono diff_subset

Premises used: Set.diff_subset, ENNReal.natCast_lt_top, LT.lt.trans_le', ENNReal.mul_lt_top, MeasureTheory.measure_mono, MeasureTheory.measure_ball_lt_top
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.mul_lt_top (ENNReal.natCast_lt_top _) <|
      measure_ball_lt_top.trans_le' <| measure_mono diff_subset

Premises used: Set.diff_subset, ENNReal.natCast_lt_top, LT.lt.trans_le', ENNReal.mul_lt_top, MeasureTheory.measure_mono, MeasureTheory.measure_ball_lt_top
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
⊢ 0 ≤ (↑x : ℝ)

Tactic:
have hr₀ : 0 ≤ x.1 := le_of_lt x.2
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
hr₀ : 0 ≤ (↑x : ℝ)
⊢ ENNReal.ofReal (∫ (x : ℝ) in 0..(↑x : ℝ), x ^ n) = ENNReal.ofReal ((↑x : ℝ) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
hr₀ : 0 ≤ (↑x : ℝ)
h : ∀ (y : ℝ) (hy : y ∈ Ioc 0 (↑x : ℝ)), 0 y ≤ y ^ n
⊢ (ae (F := Measure ℝ) (restrict volume (Ioc 0 (↑x : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ x ^ n

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioc] with y hy

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
hr₀ : 0 ≤ (↑x : ℝ)
y : ℝ
hy : y ∈ Ioc 0 (↑x : ℝ)
⊢ 0 y ≤ y ^ n

Tactic:
pow_nonneg hy.1.le _

Premises used: pow_nonneg, LT.lt.le, And.left
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
x : (↑(Ioi 0) : Type)
hr₀ : 0 ≤ (↑x : ℝ)
y : ℝ
hy : y ∈ Ioc 0 (↑x : ℝ)
⊢ 0 y ≤ y ^ n

Tactic:
exact pow_nonneg hy.1.le _

Premises used: pow_nonneg, LT.lt.le, And.left
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
n k : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((volumeIoiPow n : (a : Set (↑(Ioi 0) : Type)) → ℝ≥0∞)
        (Iio
          (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ⋯)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
simp [volumeIoiPow_apply_Iio]

Premises used: MeasureTheory.Measure.volumeIoiPow_apply_Iio
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
n : ℕ
⊢ SigmaFinite (volumeIoiPow n)

Tactic:
(finiteSpanningSetsIn_volumeIoiPow_range_Iio n).sigmaFinite

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite, MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_Iio
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)))

Tactic:
⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk, Homeomorph.measurable, Eq.symm, homeomorphUnitSphereProd
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
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)) μ))
⊢ 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)))

Tactic:
refine ⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)) μ))

Tactic:
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 ↦ ?_

Premises used: Iff.mpr, MeasureTheory.Measure.prod_eq_generateFrom, MeasurableSpace.isPiSystem_measurableSet, Set.forall_mem_range, MeasureTheory.Measure.toSphere, BorelSpace.measurable_eq, MeasurableSpace.generateFrom_measurableSet, isPiSystem_Iio, MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_Iio, MeasureTheory.Measure.toFiniteSpanningSetsIn, borel_eq_generateFrom_Iio, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
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∞)
⊢ 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 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 ↦ ?_

Premises used: Iff.mpr, MeasureTheory.Measure.prod_eq_generateFrom, MeasurableSpace.isPiSystem_measurableSet, Set.forall_mem_range, MeasureTheory.Measure.toSphere, BorelSpace.measurable_eq, MeasurableSpace.generateFrom_measurableSet, isPiSystem_Iio, MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_Iio, MeasureTheory.Measure.toFiniteSpanningSetsIn, borel_eq_generateFrom_Iio, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)
⊢ Ioo 0 (↑r : ℝ) = HSMul.hSMul (β := Set ℝ) (↑r : ℝ) (Ioo 0 1)

Tactic:
simp [LinearOrderedField.smul_Ioo r.2.out]

Premises used: Membership.mem.out, LinearOrderedField.smul_Ioo, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)
⊢ 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]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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)
⊢ 0 < dim E

Tactic:
have hpos : 0 < dim E := Module.finrank_pos
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
hb : Ne (α := ℝ) (↑(dim E) : ℝ) 0
rw : LE.le (α := ℝ) 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∞)

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₀]

Premises used: MeasureTheory.Measure.toSphere_apply_aux, Membership.mem.out, smul_assoc, MeasurableSingletonClass.measurableSet_singleton, Homeomorph.measurableEmbedding, ENNReal.ofReal_mul, Nat.cast_pred, LT.lt.le, comap_subtype_coe_apply, MeasurableSet.compl, MeasureTheory.Measure.toSphere_apply', mul_div_cancel₀, Nat.sub_add_cancel, MeasureTheory.Measure.addHaar_smul_of_nonneg, MeasurableEmbedding.map_apply, mul_right_comm, MeasureTheory.Measure.volumeIoiPow_apply_Iio, sub_add_cancel, ENNReal.ofReal_natCast, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
⊢ Ne (α := ℝ) (↑(dim E) : ℝ) 0

Tactic:
(Nat.cast_pos.2 hpos).ne'

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
⊢ LE.le (α := ℝ) 0 (↑(dim E) : ℝ)

Tactic:
Nat.cast_nonneg _

Premises used: Nat.cast_nonneg
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
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
⊢ Ne (α := ℝ) (↑(dim E) : ℝ) 0

Tactic:
exacts [(Nat.cast_pos.2 hpos).ne', Nat.cast_nonneg _]

Premises used: Iff.mpr, Nat.cast_pos, Nat.cast_nonneg, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : y ∈ ball ((1 - ε / 4) • x) (ε / 4)
⊢ dist y ((1 - ε / 4) • x) < ε / 4

Tactic:
rw [mem_ball] at hy

Premises used: Metric.mem_ball
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
linarith : 1 - ε / 4 < 0 → 4 / 4 = 1
linarith₁ : 1 - ε / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 - ε / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 - ε / 4 < 0 → 4 / 4 = 1
linarith₄ : 1 - ε / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₅ : 1 - ε / 4 < 0 → GT.gt (α := ℝ) 4 0
linarith₆ :
  1 - ε / 4 < 0 → HMul.hMul (α := ℝ) 2 (-1) + (ε - 2) + (HMul.hMul (α := ℝ) 4 1 - 1 * ε - HMul.hMul (α := ℝ) 4 0) = 0
linarith₇ : 1 - ε / 4 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 - ε / 4

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
⊢ |1 - ε / 4| = 1 - ε / 4

Tactic:
have habs : |1 - ε / 4| = 1 - ε / 4 := abs_of_nonneg (by linarith)
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
habs : |1 - ε / 4| = 1 - ε / 4
hy : dist 0 ((1 - ε / 4) • x) < ε / 4
⊢ 1 - ε / 4 < ε / 4

Tactic:
simpa [norm_smul, habs, hx] using hy

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
habs : |1 - ε / 4| = 1 - ε / 4
hy : dist 0 ((1 - ε / 4) • x) < ε / 4
⊢ 1 - ε / 4 < ε / 4

Tactic:
have : 1 - ε / 4 < ε / 4 := by simpa [norm_smul, habs, hx] using hy
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
habs : |1 - ε / 4| = 1 - ε / 4
hy : dist 0 ((1 - ε / 4) • x) < ε / 4
this : 1 - ε / 4 < ε / 4
linarith : 4 / 4 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 4 / 4 = 1
linarith₃ : HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : GT.gt (α := ℝ) 4 0
linarith₅ : 4 / 4 = 1
linarith₆ : HMul.hMul (α := ℝ) 1 4 = 4
linarith₇ : GT.gt (α := ℝ) 4 0
linarith₈ : 4 / 4 = 1
linarith₉ : HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₀ : GT.gt (α := ℝ) 4 0
linarith₁₁ : 2 * (ε - 2) + (HMul.hMul (α := ℝ) 4 1 - 1 * ε - 1 * ε) = 0
linarith₁₂ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
⊢ y ≠ 0

Tactic:
have hy₀ : y ≠ 0 := by
    rintro rfl
    have : 1 - ε / 4 < ε / 4 := by simpa [norm_smul, habs, hx] using hy
    linarith
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ ‖y‖ ≤ dist y ((1 - ε / 4) • x) + ‖(1 - ε / 4) • x‖

Tactic:
simpa using dist_triangle y ((1 - ε / 4) • x) 0

Premises used: dist_triangle, HSub.hSub, HDiv.hDiv, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ dist y ((1 - ε / 4) • x) + ‖(1 - ε / 4) • x‖ < ε / 4 + ‖(1 - ε / 4) • x‖

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ ε / 4 + ‖(1 - ε / 4) • x‖ = 1

Tactic:
simp [norm_smul, habs, hx]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ ‖y‖ < 1

Tactic:
have hy₁ : ‖y‖ < 1 := calc
    ‖y‖ ≤ dist y ((1 - ε / 4) • x) + ‖(1 - ε / 4) • x‖ := by
      simpa using dist_triangle y ((1 - ε / 4) • x) 0
    _ < ε / 4 + ‖(1 - ε / 4) • x‖ := by gcongr
    _ = 1 := by simp [norm_smul, habs, hx]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
⊢ ‖u‖ = 1

Tactic:
simp [u, hy₀, norm_smul]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
⊢ ‖u‖ = 1

Tactic:
have hu₁ : ‖u‖ = 1 := by simp [u, hy₀, norm_smul]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ 0 < ‖y‖

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ Membership.mem (γ := Set E) (sphere 0 1) u

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ (fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) ‖y‖ u = y

Tactic:
simp [u, hy₀]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
refine : u ∈ ball x ε
⊢ y ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)

Tactic:
refine ⟨‖y‖, ⟨by simpa, hy₁⟩, u, ⟨?_, by simpa⟩, by simp [u, hy₀]⟩