Let X and d be given.
Assume Hd: metric_on X d.
Assume Hseqc: sequentially_compact X (metric_topology X d).
We will prove compact_space X (metric_topology X d).
We will prove topology_on X (metric_topology X d) ∧ ∀Fam : set, open_cover_of X (metric_topology X d) Fam → has_finite_subcover X (metric_topology X d) Fam.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hd).
Let Fam be given.
Assume Hcov: open_cover_of X (metric_topology X d) Fam.
We will prove has_finite_subcover X (metric_topology X d) Fam.
Apply (sequentially_compact_metric_has_lebesgue_number_eps X d Fam Hd Hseqc Hcov) to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (lebesgue_number_metric X d Fam (eps_ N)) HNpack).
We prove the intermediate claim Hleb: lebesgue_number_metric X d Fam (eps_ N).
An exact proof term for the current goal is (andER (N ∈ ω) (lebesgue_number_metric X d Fam (eps_ N)) HNpack).
We prove the intermediate claim HexF: ∃F : set, finite_ball_cover_metric X d (eps_ N) F.
An exact proof term for the current goal is (sequentially_compact_metric_has_finite_ball_cover_eps X d N Hd Hseqc HNO).
An exact proof term for the current goal is (lebesgue_and_ball_cover_imply_finite_subcover X d Fam (eps_ N) Hd Hcov Hleb HexF).
∎