case intro.intro
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.594552
inst✝¹ : NormedAddCommGroup E
inst✝ : IsLocallyFiniteMeasure μ
x : α
ε : ℝ
εpos : 0 < ε
με : ↑↑μ (closedBall x ε) < ⊤
⊢ ∀ᶠ (a : Set α) in filterAt v x, ↑↑μ a < ⊤
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.594552
inst✝¹ : NormedAddCommGroup E
inst✝ : IsLocallyFiniteMeasure μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, ↑↑μ a < ⊤
obtain ⟨ε, εpos, με⟩ : ∃ (ε : ℝ), 0 < ε ∧ μ (closedBall x ε) < ∞ :=
  (μ.finiteAt_nhds x).exists_mem_basis nhds_basis_closedBall
no goals
case intro.intro
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.594552
inst✝¹ : NormedAddCommGroup E
inst✝ : IsLocallyFiniteMeasure μ
x : α
ε : ℝ
εpos : 0 < ε
με : ↑↑μ (closedBall x ε) < ⊤
⊢ ∀ᶠ (a : Set α) in filterAt v x, ↑↑μ a < ⊤
exact v.eventually_filterAt_iff.2 ⟨ε, εpos, fun a _ haε => (measure_mono haε).trans_lt με⟩