no goals
α : Type u_1
β : Type ?u.9479
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s₁ s₂ t₁ t₂ : Set α
x : α
s t : Set α
⊢ t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen i ∧ s ⊆ i) ∧ i ⊆ t
simp [mem_nhdsSet_iff_exists, and_assoc]