no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ s \ t ⊆ closure t ↔ s ⊆ closure t
rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]