-- 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
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)
⊢ 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∞)
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) 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∞) =
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin]