awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ dist y ((1 - ε / 4) • x) + dist ((1 - ε / 4) • x) x < ε / 4 + dist ((1 - ε / 4) • x) 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
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ ε / 4 + dist ((1 - ε / 4) • x) x = ε / 4 + ε / 4

Tactic:
simp [sub_smul, norm_smul, hx, abs_of_pos hε]

Premises used: norm_smul, sub_smul, abs_of_pos
-- 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
⊢ ε / 4 + ε / 4 = ε / 2

Tactic:
ring
-- 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
⊢ dist y x < ε / 2

Tactic:
have hyx := calc
    dist y x ≤ dist y ((1 - ε / 4) • x) + dist ((1 - ε / 4) • x) x := dist_triangle ..
    _ < ε / 4 + dist ((1 - ε / 4) • x) x := by gcongr
    _ = ε / 4 + ε / 4 := by simp [sub_smul, norm_smul, hx, abs_of_pos hε]
    _ = ε / 2 := by ring
-- 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
hyx : dist y x < ε / 2
⊢ u - y = (1 - ‖y‖) • u

Tactic:
simp [u, hy₀, sub_smul]

Premises used: sub_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
hyx : dist y x < ε / 2
⊢ u - y = (1 - ‖y‖) • u

Tactic:
have H : u - y = (1 - ‖y‖) • u := by simp [u, hy₀, sub_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
hyx : dist y x < ε / 2
H : u - y = (1 - ‖y‖) • u
⊢ dist u y ≤ dist x y

Tactic:
simpa [dist_eq_norm_sub, H, norm_smul, abs_of_nonneg, hy₁.le, hu₁, hx]
      using dist_triangle x y 0

Premises used: dist_triangle, norm_smul, dist_eq_norm_sub, LT.lt.le, abs_of_nonneg, 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
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
hyx : dist y x < ε / 2
⊢ dist u y ≤ dist x y

Tactic:
have huy : dist u y ≤ dist x y := by
    have H : u - y = (1 - ‖y‖) • u := by simp [u, hy₀, sub_smul]
    simpa [dist_eq_norm_sub, H, norm_smul, abs_of_nonneg, hy₁.le, hu₁, hx]
      using dist_triangle x y 0
-- 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
hyx : dist y x < ε / 2
huy : dist u y ≤ dist x y
linarith : ε ≤ dist u x → 2 / 2 = 1
linarith₁ : ε ≤ dist u x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε ≤ dist u x → GT.gt (α := ℝ) 2 0
linarith₃ : ε ≤ dist u x → 4 / 4 = 1
linarith₄ : ε ≤ dist u x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₅ : ε ≤ dist u x → GT.gt (α := ℝ) 4 0
linarith₆ : ε ≤ dist u x → 4 / 4 = 1
linarith₇ : ε ≤ dist u x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₈ : ε ≤ dist u x → GT.gt (α := ℝ) 4 0
linarith₉ :
  ε ≤ dist u x →
    2 * dist y x - 1 * ε + (dist u y - dist x y) + (ε - dist u x) + (dist u x - (dist u y + dist y x)) +
        (dist x y - dist y x) =
      0
⊢ dist u x < ε

Tactic:
linarith [dist_triangle u y x, dist_comm x y]

Premises used: dist_triangle, dist_comm
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
ε : ℝ
unfold : 0 < if n ≠ 0 ∧ 0 < ε then (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n else 1
⊢ 0 < toSphereBallBound n ε

Tactic:
unfold toSphereBallBound

Premises used: MeasureTheory.Measure.toSphereBallBound
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
ε : ℝ
pos : ∀ (h : n ≠ 0 ∧ 0 < ε), 0 < (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n
neg : ∀ (h : ¬(n ≠ 0 ∧ 0 < ε)), LT.lt (α := ℝ≥0) 0 1
⊢ 0 < if n ≠ 0 ∧ 0 < ε then (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n else 1

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
⊢ n ≠ 0

Tactic:
cases h
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
left : n ≠ 0
⊢ 0 < ε

Tactic:
cases h
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
ε : ℝ
left : n ≠ 0
right : 0 < ε
⊢ 0 < (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
n : ℕ
ε : ℝ
h : ¬(n ≠ 0 ∧ 0 < ε)
⊢ LT.lt (α := ℝ≥0) 0 1

Tactic:
positivity
-- 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ε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
⊢ ‖(↑x : E)‖ ≠ norm.{u_1} (E := E) 0

Tactic:
simp
-- 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ε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
⊢ Nontrivial E

Tactic:
have : Nontrivial E := ⟨⟨x, 0, ne_of_apply_ne Norm.norm (by simp)⟩⟩
-- 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ε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
inr :
  ∀
    (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),
    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 ε)
wlog :
  ∀ {ε : ℝ} (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 ε)
⊢ 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 ε)

Tactic:
wlog hε₂ : ε ≤ 2 generalizing ε
-- 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ε : 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
trans :
  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 (min ε 2))
trans₁ :
  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∞)
⊢ 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 ε)

Tactic:
trans μ.toSphere (ball x (min ε 2))

Premises used: MeasureTheory.Measure.toSphere, Metric.ball, OfNat.ofNat, DFunLike.coe, Min.min
-- 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ε : 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
⊢ 0 < min ε 2

Tactic:
simp [hε]
-- 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ε : 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
⊢ min ε 2 ≤ 2

Tactic:
simp
-- 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ε : 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
⊢ 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 (min ε 2))

Tactic:
simpa [Real.toNNReal_monotone.map_min, toSphereBallBound]
        using this (ε := min ε 2) (by simp [hε]) (by simp)

Premises used: Real.toNNReal_monotone, MeasureTheory.Measure.toSphereBallBound, Monotone.map_min
-- 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ε : 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
h : min ε 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∞)

Tactic:
gcongr
-- 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ε : 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
⊢ min ε 2 ≤ ε

Tactic:
simp
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
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∞)
⊢ 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 ε)

Tactic:
rw [μ.toSphere_apply' measurableSet_ball, Subtype.image_ball, setOf_mem_eq]

Premises used: MeasureTheory.Measure.toSphere_apply', Set.setOf_mem_eq, measurableSet_ball, Subtype.image_ball
-- 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
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∞)
hx : ‖(↑x : E)‖ = 1
hε₁ : 0 < ε
hε2 : ε ≤ 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∞)

Tactic:
grw [← ball_subset_sector_of_small_epsilon]

Premises used: _private.0.MeasureTheory.Measure.ball_subset_sector_of_small_epsilon
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

Tactic:
assumption
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

Tactic:
try assumption
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2

Tactic:
assumption
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2

Tactic:
try assumption
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ dim E ≠ 0

Tactic:
have hdim : Module.finrank ℝ E ≠ 0 := Module.finrank_pos.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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
hdim : dim E ≠ 0
⊢ min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε

Tactic:
simpa
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
hdim : dim E ≠ 0
⊢ min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε

Tactic:
have : min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε := by simpa
-- 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
x : (↑(sphere 0 1) : Type u_1)
this_1 : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
hdim : dim E ≠ 0
this : min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε
⊢ 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:
simp (disch := positivity) [μ.addHaar_ball_of_pos (r := ε / 4), ENNReal.ofReal_div_of_pos,
      toSphereBallBound, mul_assoc, ENNReal.ofNNReal_toNNReal, this, hdim, hε]

Premises used: ENNReal.ofNNReal_toNNReal, MeasureTheory.Measure.addHaar_ball_of_pos, ENNReal.ofReal_div_of_pos, mul_assoc, MeasureTheory.Measure.toSphereBallBound
-- 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
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ‖(↑x : 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
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
h₂ :
  Ne (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)) ∞
⊢ (↑(toSphereBallBound (dim E) ε) : ℝ) * μ.real (ball 0 1) ≤ Measure.real μ.toSphere (ball x ε)

Tactic:
grw [Measure.real, Measure.real, ← toSphereBallBound_mul_measure_unitBall_le_toSphere_ball μ hε,
    ENNReal.toReal_mul, ENNReal.coe_toReal]

Premises used: ENNReal.coe_toReal, MeasureTheory.Measure.real, ENNReal.toReal_mul, MeasureTheory.Measure.toSphereBallBound_mul_measure_unitBall_le_toSphere_ball
-- 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ε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
⊢ Ne (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)) ∞

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
⊢ @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 _)
-- 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 _ _ _ (↑{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 _ _ _ (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

Premises used: Function.comp_def, homeomorphUnitSphereProd_apply_snd_coe