no goals
α✝ : Type u
β : Type v
ι : Type ?u.47137
π : ι → Type ?u.47142
inst✝³ : TopologicalSpace α✝
inst✝² : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ cocompact α = cofinite
simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]