no goals
X : Type u_1
Y : Type ?u.22819
inst✝¹ : UniformSpace X
s : Set X
inst✝ : IsCountablyGenerated (𝓤 X)
⊢ CompactSpace X ↔ SeqCompactSpace X
simp only [← isCompact_univ_iff, seqCompactSpace_iff, UniformSpace.isCompact_iff_isSeqCompact]