no goals
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
P : Set α → Prop
⊢ (∃ᶠ (a : Set α) in filterAt v x, P a) ↔ ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ P a
simp only [Filter.Frequently, eventually_filterAt_iff, not_exists, exists_prop, not_and,
  Classical.not_not, not_forall]