Let X and Tx be given.
Assume Hcomp: compact_space X Tx.
We will prove Lindelof_space X Tx.
We will prove topology_on X Tx ∧ ∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V.
Apply andI to the current goal.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
Let U be given.
Assume HU: open_cover X Tx U.
We will prove ∃V : set, countable_subcollection V U ∧ covers X V.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim HUof: open_cover_of X Tx U.
An exact proof term for the current goal is (open_cover_implies_open_cover_of X Tx U HTx HU).
We prove the intermediate claim Hfin: has_finite_subcover X Tx U.
An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp U HUof).
Set G to be the term Eps_i (λG0 : set ⇒ G0 ⊆ U ∧ finite G0 ∧ X ⊆ ⋃ G0).
We prove the intermediate claim HG: G ⊆ U ∧ finite G ∧ X ⊆ ⋃ G.
An exact proof term for the current goal is (Eps_i_ex (λG0 : set ⇒ G0 ⊆ U ∧ finite G0 ∧ X ⊆ ⋃ G0) Hfin).
We use G to witness the existential quantifier.
Apply andI to the current goal.
We will prove countable_subcollection G U.
We prove the intermediate claim HG1: G ⊆ U ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ U ∧ finite G) (X ⊆ ⋃ G) HG).
We prove the intermediate claim HGsub: G ⊆ U.
An exact proof term for the current goal is (andEL (G ⊆ U) (finite G) HG1).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ U) (finite G) HG1).
An exact proof term for the current goal is (andI (G ⊆ U) (countable_set G) HGsub (finite_countable G HGfin)).
We prove the intermediate claim HsubU: X ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ U ∧ finite G) (X ⊆ ⋃ G) HG).
An exact proof term for the current goal is (Subq_Union_implies_covers X G HsubU).
∎