no goals
α : Type u
β : Type v
ι : Type ?u.52091
π : ι → Type ?u.52096
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
⊢ s ∈ coclosedCompact α ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ s
simp only [hasBasis_coclosedCompact.mem_iff, and_assoc]