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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
⊢ Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))

Tactic:
have B :
    Tendsto (fun r : ℝ => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0)
      (𝓝 (μ (closedBall x 1) / μ ({x} + u))) := by
    apply tendsto_const_nhds.congr' _
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    have : closedBall x r = {x} + r • closedBall (0 : E) 1 := by
      simp only [_root_.smul_closedBall, Real.norm_of_nonneg rpos.le, zero_le_one, add_zero,
        mul_one, singleton_add_closedBall, smul_zero]
    simp only [this, addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne']
    simp only [addHaar_closedBall_center, image_add_left, measure_preimage_add, singleton_add]
-- 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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
apply :
  Ne (α := ℝ≥0∞) 0 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞) ≠
      ∞
⊢ Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (0 *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))

Tactic:
apply ENNReal.Tendsto.mul A _ B (Or.inr ENNReal.zero_ne_top)

Premises used: ENNReal.Tendsto.mul, ENNReal.zero_ne_top, Or.inr
-- 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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
⊢ Ne (α := ℝ≥0∞) 0 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞) ≠
      ∞

Tactic:
simp [ENNReal.div_eq_top, h'u, measure_closedBall_lt_top.ne]

Premises used: ENNReal.div_eq_top, 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
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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
⊢ Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (0 *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))

Tactic:
have C : Tendsto (fun r : ℝ =>
        μ (s ∩ ({x} + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({x} + r • u)))
      (𝓝[>] 0) (𝓝 (0 * (μ (closedBall x 1) / μ ({x} + u)))) := by
    apply ENNReal.Tendsto.mul A _ B (Or.inr ENNReal.zero_ne_top)
    simp [ENNReal.div_eq_top, h'u, measure_closedBall_lt_top.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
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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
C :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (0 *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)

Tactic:
simp only [zero_mul] at C

Premises used: MulZeroClass.zero_mul
-- 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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
C :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
apply :
  EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)

Tactic:
apply C.congr' _

Premises used: 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
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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
C :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t)) : ℝ≥0∞)
            ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞) *
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
            ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • u) : ℝ≥0∞) =
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • u) : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥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
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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
C :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
simp :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) (closedBall x r))⁻¹ : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u))⁻¹ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) (closedBall x r))⁻¹ : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u))⁻¹ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥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 ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- 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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
C :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) (closedBall x r))⁻¹ : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u))⁻¹ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) (closedBall x r))⁻¹ : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u))⁻¹ : ℝ≥0∞)

Tactic:
ring
-- 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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
B :
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))
C :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) *
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
rw :
  1 *
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)
rw₁ rw₂ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥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 ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)

Tactic:
rw [ENNReal.mul_inv_cancel (measure_closedBall_pos μ x rpos).ne'
          measure_closedBall_lt_top.ne,
        one_mul]

Premises used: LT.lt.ne', ENNReal.mul_inv_cancel, Metric.measure_closedBall_pos, MeasureTheory.measure_closedBall_lt_top, one_mul, 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
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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
⊢ let t' := R⁻¹ • t;
  t' = R⁻¹ • t

Tactic:
set t' := R⁻¹ • t with ht'
-- 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 u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
⊢ let u' := R⁻¹ • u;
  u' = R⁻¹ • u

Tactic:
set u' := R⁻¹ • u with hu'