feat(Topology/Compactness): add missing instances for countably compact (leanprover-community#37460)

Co-authored-by: Batixx <s59fpern@uni-bonn.de>

Author: felixpernegger

Mathlib/Topology/Compactness/CountablyCompact.lean

@@ -167,18 +167,35 @@ theorem isCountablyCompact_iff_countable_open_cover' :
 theorem IsCompact.isCountablyCompact (hA : IsCompact A) : IsCountablyCompact A :=
   fun _ _ _ hle => hA hle
 
+/-- A compact space is countably compact. -/
+instance CompactSpace.CountablyCompactSpace
+    {X : Type*} [TopologicalSpace X] [CompactSpace X] :
+    CountablyCompactSpace X where
+  isCountablyCompact_univ := isCompact_univ.isCountablyCompact
+
 /-- A sequentially compact set is countably compact. -/
 theorem IsSeqCompact.isCountablyCompact (hA : IsSeqCompact A) :
     IsCountablyCompact A := IsCountablyCompact.of_seq_clusterPt fun x hx => by
   obtain ⟨a, ha, φ, hφ, hφa⟩ := hA.subseq_of_frequently_in hx.frequently
   exact ⟨a, ha, hφa.mapClusterPt.of_comp hφ.tendsto_atTop⟩
 
+/-- A sequentially compact space is countably compact. -/
+instance SeqCompactSpace.CountablyCompactSpace
+    {X : Type*} [TopologicalSpace X] [SeqCompactSpace X] :
+    CountablyCompactSpace X where
+  isCountablyCompact_univ := isSeqCompact_univ.isCountablyCompact
+
 /-- In a first-countable space, a countably compact set is sequentially compact. -/
 theorem IsCountablyCompact.isSeqCompact [FirstCountableTopology E]
     (hA : IsCountablyCompact A) : IsSeqCompact A := fun x hx =>
     let ⟨a, haA, hac⟩ := IsCountablyCompact.seq_clusterPt hA x (Eventually.of_forall hx)
     ⟨a, haA, TopologicalSpace.FirstCountableTopology.tendsto_subseq hac⟩
 
+/-- In a first-countable countably compact space is sequentially compact. -/
+instance CountablyCompactSpace.SeqCompactSpace {X : Type*} [TopologicalSpace X]
+    [FirstCountableTopology X] [CountablyCompactSpace X] : SeqCompactSpace X where
+    isSeqCompact_univ := isCountablyCompact_univ.isSeqCompact
+
 /-- In a first-countable space, a set is countably compact iff it is sequentially compact. -/
 theorem isCountablyCompact_iff_isSeqCompact [FirstCountableTopology E] :
     IsCountablyCompact A ↔ IsSeqCompact A :=
@@ -231,6 +248,11 @@ theorem IsLindelof.isCompact (hA : IsCountablyCompact A) (hl : IsLindelof A) :
     exact ⟨t.image f, by simp_all⟩
   · exact ⟨∅, by simp_all⟩
 
+/-- A countably compact Lindelöf space is compact. -/
+theorem LindelofSpace.CompactSpace {X : Type*} [TopologicalSpace X]
+    [LindelofSpace X] [h : CountablyCompactSpace X] : CompactSpace X where
+    isCompact_univ := isLindelof_univ.isCompact h.isCountablyCompact_univ
+
 /-- In a Hereditarily Lindelöf space, a countably compact set is compact. -/
 theorem IsCountablyCompact.isCompact [HereditarilyLindelofSpace E]
     (hA : IsCountablyCompact A) : IsCompact A :=