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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x a) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
h₁ : s = sᶜᶜ
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) -
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
convert!
      I (closedBall x r) sᶜ (measure_closedBall_pos μ _ rpos).ne' measure_closedBall_lt_top.ne
        hs.compl

Premises used: Compl.compl, MeasurableSet.compl, LT.lt.ne', Metric.measure_closedBall_pos, Metric.closedBall, MeasureTheory.measure_closedBall_lt_top, LT.lt.ne
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x a) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
h₁ h₂ : s = s
⊢ s = sᶜᶜ

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
⊢ 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)

Tactic:
have L : Tendsto (fun r => μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) := by
    have A : Tendsto (fun r => μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1) := by
      apply tendsto_const_nhds.congr' _
      filter_upwards [self_mem_nhdsWithin]
      intro r hr
      rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]
      · exact (measure_closedBall_pos μ _ hr).ne'
      · exact measure_closedBall_lt_top.ne
    have B := ENNReal.Tendsto.sub A h (Or.inl ENNReal.one_ne_top)
    simp only [tsub_self] at B
    apply B.congr' _
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    convert!
      I (closedBall x r) sᶜ (measure_closedBall_pos μ _ rpos).ne' measure_closedBall_lt_top.ne
        hs.compl
    rw [compl_compl]
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)

Tactic:
have L' : Tendsto (fun r : ℝ => μ (sᶜ ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0) :=
    tendsto_addHaar_inter_smul_zero_of_density_zero μ sᶜ x L t ht 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
L' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
apply :
  EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
apply tendsto_const_nhds.congr' _

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
L' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      1 =
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
L' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
have L'' : Tendsto (fun r : ℝ => μ ({x} + r • t) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 1) := by
    apply tendsto_const_nhds.congr' _
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    rw [addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne', ENNReal.div_self h't 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
L' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
L'' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
⊢ Tendsto
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (HSub.hSub (α := ℝ≥0∞) 1 0))

Tactic:
have := ENNReal.Tendsto.sub L'' L' (Or.inl ENNReal.one_ne_top)
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
L' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
L'' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
this :
  Tendsto
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (HSub.hSub (α := ℝ≥0∞) 1 0))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
simp only [tsub_zero] at this

Premises used: tsub_zero
-- 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
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
L :
  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)
L' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
L'' :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
apply :
  EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞) -
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞))
    fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
apply this.congr' _

Premises used: Filter.Tendsto.congr'