no goals
α : Type u_1
β : Type ?u.11087
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
hU : IsOpen s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s
rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]