awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
⊢ 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∞)

Tactic:
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)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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ᶜ = ∅
simp_rw₅ : t ∩ ∅ = ∅
⊢ Eq.{u_1 + 1} (α := Set E) (⋂ (n : ℕ), t \ closedBall 0 (↑n : ℝ)) ∅

Tactic:
simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]

Premises used: compl_compl, Set.iInter_eq_compl_iUnion_compl, Set.diff_eq, Set.compl_univ, Set.inter_iInter, Set.inter_empty, Metric.iUnion_closedBall_nat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 : ℝ)) ∅
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ))) atTop (𝓝 0)

Tactic:
simp only [this, measure_empty] at A

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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)
I : 0 < HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (n : ℕ),
    0 < n ∧
      (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
        HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists

Premises used: tendsto_order, Filter.Eventually.and, Filter.Ioi_mem_atTop, Filter.Eventually.exists, And.right, Iff.mp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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)
I : 0 < HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (n : ℕ),
    0 < n ∧
      (μ : (a : Set E) → ℝ≥0∞) (t \ closedBall 0 (↑n : ℝ)) <
        HMul.hMul (β := ℝ≥0∞) (ε / 2) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists

Premises used: tendsto_order, Filter.Eventually.and, Filter.Ioi_mem_atTop, Filter.Eventually.exists, And.right, Iff.mp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
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∞) <
        ε
⊢ ∀ᶠ (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

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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)
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∞) <
          ε
⊢ ∀ᶠ (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:
filter_upwards [(tendsto_order.1 L).2 _ (ENNReal.half_pos εpos.ne'), self_mem_nhdsWithin]

Premises used: tendsto_order, LT.lt.ne', And.right, self_mem_nhdsWithin, ENNReal.half_pos, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
rw₃ rw₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥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∞)

Tactic:
rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]

Premises used: Set.smul_set_union, Set.inter_union_diff, Set.inter_union_distrib_left, Set.add_union
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
bc : s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ))) ⊆ {x} + r • (t \ closedBall 0 (↑n : ℝ))
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • (t \ closedBall 0 (↑n : ℝ))) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
⊢ s ∩ ({x} + r • (t \ closedBall 0 (↑n : ℝ))) ⊆ {x} + r • (t \ closedBall 0 (↑n : ℝ))

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
⊢ (μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • (t \ closedBall 0 (↑n : ℝ))) : ℝ≥0∞)

Tactic:
have I :
    μ (s ∩ ({x} + r • t)) ≤
      μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n)) :=
    calc
      μ (s ∩ ({x} + r • t)) =
          μ (s ∩ ({x} + r • (t ∩ closedBall 0 n)) ∪ s ∩ ({x} + r • (t \ closedBall 0 n))) := by
        rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]
      _ ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ (s ∩ ({x} + r • (t \ closedBall 0 n))) :=
        measure_union_le _ _
      _ ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n)) := by
        gcongr; apply inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
I :
  (μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • (t \ closedBall 0 (↑n : ℝ))) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) ≤
    HDiv.hDiv (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • (t ∩ closedBall 0 (↑n : ℝ)))) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • (t \ closedBall 0 (↑n : ℝ))) : ℝ≥0∞))
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)

Tactic:
gcongr