no goals
α : Type u
β : Type v
ι : Type ?u.52679
π : ι → Type ?u.52684
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ s ∈ coclosedCompact α ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ sᶜ ⊆ t
simp only [mem_coclosedCompact, compl_subset_comm]