no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ interior s ↔ x ∈ {a | s ∈ 𝓝 a}
simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]