no goals
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, MeasurableSet a
filter_upwards [v.eventually_filterAt_mem_sets x]with _ ha using v.MeasurableSet' _ _ ha