no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
h : ∀ (V : Set (α × α)), V ∈ 𝓤 α → SymmetricRel V → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y V
V : Set (α × α)
hV : V ∈ 𝓤 α ∧ SymmetricRel V
⊢ ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ id V}
simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2