Let X, d, Fam and delta be given.
Assume Hd: metric_on X d.
Assume Hcov: open_cover_of X (metric_topology X d) Fam.
Assume Hleb: lebesgue_number_metric X d Fam delta.
Assume HexF: ∃F : set, finite_ball_cover_metric X d delta F.
We will prove has_finite_subcover X (metric_topology X d) Fam.
Apply HexF to the current goal.
Let F be given.
Assume HFcover: finite_ball_cover_metric X d delta F.
We prove the intermediate claim HFpair: finite F ∧ F ⊆ X.
An exact proof term for the current goal is (andEL (finite F ∧ F ⊆ X) (X ⊆ (⋃c ∈ Fopen_ball X d c delta)) HFcover).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (andEL (finite F) (F ⊆ X) HFpair).
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (andER (finite F) (F ⊆ X) HFpair).
We prove the intermediate claim HXcov: X ⊆ (⋃c ∈ Fopen_ball X d c delta).
An exact proof term for the current goal is (andER (finite F ∧ F ⊆ X) (X ⊆ (⋃c ∈ Fopen_ball X d c delta)) HFcover).
We prove the intermediate claim Hleb3: ∀x : set, x ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x delta ⊆ U.
An exact proof term for the current goal is (andER (delta ∈ R ∧ Rlt 0 delta) (∀x0 : set, x0 ∈ X → ∃U : set, U ∈ Fam ∧ open_ball X d x0 delta ⊆ U) Hleb).
Set pickU to be the term (λc : set ⇒ Eps_i (λU : set ⇒ U ∈ Fam ∧ open_ball X d c delta ⊆ U)).
We prove the intermediate claim HpickU: ∀c : set, c ∈ F → pickU c ∈ Fam ∧ open_ball X d c delta ⊆ pickU c.
Let c be given.
Assume HcF: c ∈ F.
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (HFsubX c HcF).
We prove the intermediate claim HexU: ∃U : set, U ∈ Fam ∧ open_ball X d c delta ⊆ U.
An exact proof term for the current goal is (Hleb3 c HcX).
Apply HexU to the current goal.
Let U be given.
Assume HU: U ∈ Fam ∧ open_ball X d c delta ⊆ U.
An exact proof term for the current goal is (Eps_i_ax (λU0 : set ⇒ U0 ∈ Fam ∧ open_ball X d c delta ⊆ U0) U HU).
Set G to be the term {pickU c|c ∈ F}.
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (Repl_finite pickU F HFfin).
We prove the intermediate claim HGsub: G ⊆ Fam.
Let U be given.
Assume HU: U ∈ G.
We prove the intermediate claim Hexc: ∃c ∈ F, U = pickU c.
An exact proof term for the current goal is (ReplE F pickU U HU).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcF: c ∈ F.
An exact proof term for the current goal is (andEL (c ∈ F) (U = pickU c) Hcpair).
We prove the intermediate claim HUeq: U = pickU c.
An exact proof term for the current goal is (andER (c ∈ F) (U = pickU c) Hcpair).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (andEL (pickU c ∈ Fam) (open_ball X d c delta ⊆ pickU c) (HpickU c HcF)).
We prove the intermediate claim HXsubUnionG: X ⊆ ⋃ G.
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ G.
We prove the intermediate claim HxCov: x ∈ (⋃c ∈ Fopen_ball X d c delta).
An exact proof term for the current goal is (HXcov x HxX).
Apply (famunionE_impred F (λc : set ⇒ open_ball X d c delta) x HxCov (x ∈ ⋃ G)) to the current goal.
Let c be given.
Assume HcF: c ∈ F.
Assume HxBall: x ∈ open_ball X d c delta.
We prove the intermediate claim HUinFam: pickU c ∈ Fam.
An exact proof term for the current goal is (andEL (pickU c ∈ Fam) (open_ball X d c delta ⊆ pickU c) (HpickU c HcF)).
We prove the intermediate claim HBallSub: open_ball X d c delta ⊆ pickU c.
An exact proof term for the current goal is (andER (pickU c ∈ Fam) (open_ball X d c delta ⊆ pickU c) (HpickU c HcF)).
We prove the intermediate claim HxU: x ∈ pickU c.
An exact proof term for the current goal is (HBallSub x HxBall).
We prove the intermediate claim HpUinG: pickU c ∈ G.
An exact proof term for the current goal is (ReplI F pickU c HcF).
An exact proof term for the current goal is (UnionI G x (pickU c) HxU HpUinG).
Apply (has_finite_subcoverI X (metric_topology X d) Fam G) to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HGsub.
An exact proof term for the current goal is HGfin.
An exact proof term for the current goal is HXsubUnionG.
∎