no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.130486
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
⊢ coclosedCompact α = cocompact α
simp only [coclosedCompact, cocompact, iInf_and',
  and_iff_right_of_imp (@IsCompact.isClosed α _ _ _)]