no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h : IsOpen s
⊢ closure (s ∩ t)ᶜ ⊆ (s ∩ closure t)ᶜ
simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl