awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
h : 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
⊢ ((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 rw : LE.le (α := ℝ) 0 (↑(dim E) : ℝ)
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₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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)
⊢ y ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)
have hy₁ : dist y ((1 - ε / 4) • x) < ε / 4
Tactic: rw [mem_ball] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ 0 ≤ 1 - ε / 4
have linarith : 1 - ε / 4 < 0 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ 0 ≤ 1 - ε / 4
have linarith₁ : 1 - ε / 4 < 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ 0 ≤ 1 - ε / 4
have linarith₂ : 1 - ε / 4 < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ 0 ≤ 1 - ε / 4
have linarith₆ : 1 - ε / 4 < 0 → HMul.hMul (α := ℝ) 2 (-1) + (ε - 2) + (HMul.hMul (α := ℝ) 4 1 - 1 * ε - HMul.hMul (α := ℝ) 4 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ 0 ≤ 1 - ε / 4
have linarith₇ : 1 - ε / 4 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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
⊢ y ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)
have habs : |1 - ε / 4| = 1 - ε / 4
Tactic: have habs : |1 - ε / 4| = 1 - ε / 4 := abs_of_nonneg (by linarith)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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
⊢ False
have this : 1 - ε / 4 < ε / 4
Tactic: have : 1 - ε / 4 < ε / 4 := by simpa [norm_smul, habs, hx] using hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ False
have linarith : 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ False
have linarith₄ : GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ False
have linarith₁₁ : 2 * (ε - 2) + (HMul.hMul (α := ℝ) 4 1 - 1 * ε - 1 * ε) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ False
have linarith₁₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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 ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)
have hy₀ : y ≠ 0
Tactic: have hy₀ : y ≠ 0 := by
    rintro rfl
    have : 1 - ε / 4 < ε / 4 := by simpa [norm_smul, habs, hx] using hy
    linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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 ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)
have hy₁ : ‖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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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
⊢ y ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)
have hu₁ : ‖u‖ = 1
Tactic: have hu₁ : ‖u‖ = 1 := by simp [u, hy₀, norm_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ y ∈ HSMul.hSMul (α := Set ℝ) (Ioo 0 1) (ball x ε ∩ sphere 0 1)
have refine : u ∈ ball x ε
Tactic: refine ⟨‖y‖, ⟨by simpa, hy₁⟩, u, ⟨?_, by simpa⟩, by simp [u, hy₀]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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 u x < ε
have hyx : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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
have H : u - y = (1 - ‖y‖) • u
Tactic: have H : u - y = (1 - ‖y‖) • u := by simp [u, hy₀, sub_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
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 x < ε
have huy : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have linarith : ε ≤ dist u x → 2 / 2 = 1
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have linarith₁ : ε ≤ dist u x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have linarith₂ : ε ≤ dist u x → GT.gt (α := ℝ) 2 0
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have linarith₃ : ε ≤ dist u x → 4 / 4 = 1
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have linarith₄ : ε ≤ dist u x → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have linarith₅ : ε ≤ dist u x → GT.gt (α := ℝ) 4 0
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
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
⊢ dist u x < ε
have 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
Tactic: linarith [dist_triangle u y x, dist_comm x y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
n : ℕ
ε : ℝ
⊢ 0 < toSphereBallBound n ε
have unfold : 0 < if n ≠ 0 ∧ 0 < ε then (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n else 1
Tactic: unfold toSphereBallBound
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
n : ℕ
ε : ℝ
⊢ 0 < if n ≠ 0 ∧ 0 < ε then (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n else 1
have pos : ∀ (h : n ≠ 0 ∧ 0 < ε), 0 < (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
n : ℕ
ε : ℝ
pos : ∀ (h : n ≠ 0 ∧ 0 < ε), 0 < (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n
⊢ 0 < if n ≠ 0 ∧ 0 < ε then (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n else 1
have neg : ∀ (h : ¬(n ≠ 0 ∧ 0 < ε)), LT.lt (α := ℝ≥0) 0 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
Goal:
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
⊢ 0 < (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n
have left : n ≠ 0
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (hypothesis)
Goal:
n : ℕ
ε : ℝ
h : n ≠ 0 ∧ 0 < ε
left : n ≠ 0
⊢ 0 < (↑n : ℝ≥0) * (min ε.toNNReal 2 / 4) ^ n
have right : 0 < ε
Tactic: cases h
Cleared hypotheses: h
-- 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ε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
have this : Nontrivial E
Tactic: have : Nontrivial E := ⟨⟨x, 0, ne_of_apply_ne Norm.norm (by simp)⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
this : Nontrivial E
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
have 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 ε)
Tactic: wlog hε₂ : ε ≤ 2 generalizing ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
this : 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 ε)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
have 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 ε)
Tactic: wlog hε₂ : ε ≤ 2 generalizing ε
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
this_1 : Nontrivial E
this :
  ∀ {ε : ℝ} (hε : 0 < ε) (hε₂ : ε ≤ 2),
    HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
      ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
hε₂ : ¬ε ≤ 2
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
have 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))
Tactic: trans μ.toSphere (ball x (min ε 2))
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.HaarToSphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : (↑(sphere 0 1) : Type u_1)
this_1 : Nontrivial E
this :
  ∀ {ε : ℝ} (hε : 0 < ε) (hε₂ : ε ≤ 2),
    HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
      ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
hε₂ : ¬ε ≤ 2
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))
⊢ HMul.hMul (β := ℝ≥0∞) (↑(toSphereBallBound (dim E) ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) ≤
    ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) (ball x ε)
have 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∞)
Tactic: trans μ.toSphere (ball x (min ε 2))