no goals
α : Type u_1
β : Type ?u.7780
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s
simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]