awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
simp_rw : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t ∩ (closedBall 0 (↑n : ℝ))ᶜ) ∅
⊢ Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
have simp_rw₁ : t ∩ ⋂ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜ = ∅
Tactic: simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
simp_rw : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t ∩ (closedBall 0 (↑n : ℝ))ᶜ) ∅
simp_rw₁ : t ∩ ⋂ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜ = ∅
⊢ Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
have simp_rw₂ : t ∩ (⋃ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜᶜ)ᶜ = ∅
Tactic: simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
simp_rw : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t ∩ (closedBall 0 (↑n : ℝ))ᶜ) ∅
simp_rw₁ : t ∩ ⋂ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜ = ∅
simp_rw₂ : t ∩ (⋃ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜᶜ)ᶜ = ∅
⊢ Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
have simp_rw₃ : t ∩ (⋃ (i : ℕ), closedBall 0 (↑i : ℝ))ᶜ = ∅
Tactic: simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
simp_rw : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t ∩ (closedBall 0 (↑n : ℝ))ᶜ) ∅
simp_rw₁ : t ∩ ⋂ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜ = ∅
simp_rw₂ : t ∩ (⋃ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜᶜ)ᶜ = ∅
simp_rw₃ : t ∩ (⋃ (i : ℕ), closedBall 0 (↑i : ℝ))ᶜ = ∅
⊢ Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
have simp_rw₄ : t ∩ univᶜ = ∅
Tactic: simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
simp_rw : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t ∩ (closedBall 0 (↑n : ℝ))ᶜ) ∅
simp_rw₁ : t ∩ ⋂ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜ = ∅
simp_rw₂ : t ∩ (⋃ (i : ℕ), (closedBall 0 (↑i : ℝ))ᶜᶜ)ᶜ = ∅
simp_rw₃ : t ∩ (⋃ (i : ℕ), closedBall 0 (↑i : ℝ))ᶜ = ∅
simp_rw₄ : t ∩ univᶜ = ∅
⊢ Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
have simp_rw₅ : t ∩ ∅ = ∅
Tactic: simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
⊢ ∃ (n : ℕ),
    0 < n ∧
      (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
        HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have this : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
Tactic: have : ⋂ n : ℕ, t \ closedBall 0 n = ∅ := by
      simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ))) : Filter ℝ≥0∞)
this : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
⊢ ∃ (n : ℕ),
    0 < n ∧
      (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
        HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have A₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ))) atTop (𝓝 0)
Tactic: simp only [this, measure_empty] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅
A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ))) atTop (𝓝 0)
⊢ ∃ (n : ℕ),
    0 < n ∧
      (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
        HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have I : 0 < HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have I : 0 < ε / 2 * μ t := ENNReal.mul_pos (ENNReal.half_pos εpos.ne').ne' h't
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + b • t) : ℝ≥0∞) <
      ε
have inr : ∀ (n : ℕ) (npos : 0 < n)
  (hn :
    (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
      HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)),
  ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + b • t) : ℝ≥0∞) <
      ε
Tactic: obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ μ (t \ closedBall 0 n) < ε / 2 * μ t := by
    have A :
      Tendsto (fun n : ℕ => μ (t \ closedBall 0 n)) atTop
        (𝓝 (μ (⋂ n : ℕ, t \ closedBall 0 n))) := by
      have N : ∃ n : ℕ, μ (t \ closedBall 0 n) ≠ ∞ :=
        ⟨0, ((measure_mono diff_subset).trans_lt h''t.lt_top).ne⟩
      refine tendsto_measure_iInter_atTop
        (fun n ↦ (ht.diff measurableSet_closedBall).nullMeasurableSet) (fun m n hmn ↦ ?_) N
      exact diff_subset_diff Subset.rfl (by gcongr)
    have : ⋂ n : ℕ, t \ closedBall 0 n = ∅ := by
      simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
    simp only [this, measure_empty] at A
    have I : 0 < ε / 2 * μ t := ENNReal.mul_pos (ENNReal.half_pos εpos.ne').ne' h't
    exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
n : ℕ
npos : 0 < n
hn :
  (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
    HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + b • t) : ℝ≥0∞) <
      ε
have L : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
  (𝓝[>] 0) (𝓝 0)
Tactic: have L :
    Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) / μ ({x} + r • t)) (𝓝[>] 0)
      (𝓝 0) :=
    tendsto_addHaar_inter_smul_zero_of_density_zero_aux2 μ s x h _ t h't n (Nat.cast_pos.2 npos)
      inter_subset_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
n : ℕ
npos : 0 < n
hn :
  (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
    HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + b • t) : ℝ≥0∞) <
      ε
have h₁ : ∀ (a : ℝ),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) <
      ε / 2 →
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) <
        ε
Tactic: filter_upwards [(tendsto_order.1 L).2 _ (ENNReal.half_pos εpos.ne'), self_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
n : ℕ
npos : 0 < n
hn :
  (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
    HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
hr :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) <
    ε / 2
rpos : 0 < r
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ))) ∪ s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ)))) :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ ({x} + r • (t \ closedBall 0 (↑n : ℝ))))) :
    ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
n : ℕ
npos : 0 < n
hn :
  (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
    HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
hr :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) <
    ε / 2
rpos : 0 < r
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ ({x} + r • (t \ closedBall 0 (↑n : ℝ))))) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ))) ∪ s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ)))) :
      ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + (r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ r • (t \ closedBall 0 (↑n : ℝ))))) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
n : ℕ
npos : 0 < n
hn :
  (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
    HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
hr :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) <
    ε / 2
rpos : 0 < r
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ ({x} + r • (t \ closedBall 0 (↑n : ℝ))))) :
      ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + (r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ r • (t \ closedBall 0 (↑n : ℝ))))) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ))) ∪ s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ)))) :
      ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ) ∪ t \ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
εpos : 0 < ε
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
n : ℕ
npos : 0 < n
hn :
  (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
    HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
hr :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) <
    ε / 2
rpos : 0 < r
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ ({x} + r • (t \ closedBall 0 (↑n : ℝ))))) :
      ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + (r • (t ∩ closedBall 0 (↑n : ℝ)) ∪ r • (t \ closedBall 0 (↑n : ℝ))))) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ) ∪ t \ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ))) ∪ s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ)))) :
      ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]