α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
⊢ ∃ ε, 0 < ε
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ∈ setsAt v x
simp (config := { contextual := true }) only [eventually_filterAt_iff, exists_prop, and_true_iff,
  gt_iff_lt, imp_true_iff]
no goals
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
⊢ ∃ ε, 0 < ε
exact ⟨1, zero_lt_one⟩