Let X, d and V0 be given.
Assume Hm: metric_on X d.
Assume HV0cov: open_cover X (metric_topology X d) V0.
We will prove ∃Centers : set → set, (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n ∧ (∀c : set, c ∈ Centers n → ∃v0 : set, v0 ∈ V0 ∧ open_ball X d c (eps_ (ordsucc (ordsucc n))) ⊆ v0)) ∧ (∀x : set, x ∈ X → ∃n : set, n ∈ ω ∧ ∃c : set, c ∈ Centers n ∧ x ∈ open_ball X d c (eps_ (ordsucc (ordsucc n)))).
We prove the intermediate claim Hpoint_eps: ∀x : set, x ∈ X → ∃v0 : set, v0 ∈ V0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ v0.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (metric_open_cover_point_eps_ball_submember X d V0 x Hm HV0cov HxX).
Set pickV to be the term (λx : set ⇒ Eps_i (λv0 : set ⇒ v0 ∈ V0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ v0)).
We prove the intermediate claim HpickV: ∀x : set, x ∈ X → pickV x ∈ V0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickV x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hex: ∃v0 : set, v0 ∈ V0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ v0.
An exact proof term for the current goal is (Hpoint_eps x HxX).
Apply Hex to the current goal.
Let v0 be given.
Assume Hv0pack.
Set P to be the term (λv : set ⇒ v ∈ V0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ v).
We prove the intermediate claim Hv0P: P v0.
An exact proof term for the current goal is Hv0pack.
An exact proof term for the current goal is (Eps_i_ax P v0 Hv0P).
Set pickN to be the term (λx : set ⇒ Eps_i (λN : set ⇒ N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickV x)).
We prove the intermediate claim HpickN: ∀x : set, x ∈ X → pickN x ∈ ω ∧ open_ball X d x (eps_ (pickN x)) ⊆ pickV x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hv0pack: pickV x ∈ V0 ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickV x.
An exact proof term for the current goal is (HpickV x HxX).
We prove the intermediate claim Hex: ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickV x.
An exact proof term for the current goal is (andER (pickV x ∈ V0) (∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ pickV x) Hv0pack).
Apply Hex to the current goal.
Let N be given.
Assume HNpack.
Set Q to be the term (λN0 : set ⇒ N0 ∈ ω ∧ open_ball X d x (eps_ N0) ⊆ pickV x).
We prove the intermediate claim HNQ: Q N.
An exact proof term for the current goal is HNpack.
An exact proof term for the current goal is (Eps_i_ax Q N HNQ).
We prove the intermediate claim Hsmall_ball_in_pickV: ∀c n : set, c ∈ X → n ∈ ω → pickN c ∈ ordsucc (ordsucc n) → open_ball X d c (eps_ (ordsucc (ordsucc n))) ⊆ pickV c.
Let c and n be given.
Assume HcX: c ∈ X.
Assume HnO: n ∈ ω.
Assume HNin: pickN c ∈ ordsucc (ordsucc n).
We prove the intermediate claim HNp: pickN c ∈ ω.
An exact proof term for the current goal is (andEL (pickN c ∈ ω) (open_ball X d c (eps_ (pickN c)) ⊆ pickV c) (HpickN c HcX)).
We prove the intermediate claim HsubPick: open_ball X d c (eps_ (pickN c)) ⊆ pickV c.
An exact proof term for the current goal is (andER (pickN c ∈ ω) (open_ball X d c (eps_ (pickN c)) ⊆ pickV c) (HpickN c HcX)).
We prove the intermediate claim Hn1O: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim Hn2O: ordsucc (ordsucc n) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (ordsucc n) Hn1O).
We prove the intermediate claim Hepsn2R: eps_ (ordsucc (ordsucc n)) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc (ordsucc n))) (SNo_eps_SNoS_omega (ordsucc (ordsucc n)) Hn2O)).
We prove the intermediate claim HepsPickR: eps_ (pickN c) ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ (pickN c)) (SNo_eps_SNoS_omega (pickN c) HNp)).
We prove the intermediate claim Hlt: eps_ (ordsucc (ordsucc n)) < eps_ (pickN c).
An exact proof term for the current goal is (SNo_eps_decr (ordsucc (ordsucc n)) Hn2O (pickN c) HNin).
We prove the intermediate claim Hrl: Rlt (eps_ (ordsucc (ordsucc n))) (eps_ (pickN c)).
An exact proof term for the current goal is (RltI (eps_ (ordsucc (ordsucc n))) (eps_ (pickN c)) Hepsn2R HepsPickR Hlt).
We prove the intermediate claim Hmono: open_ball X d c (eps_ (ordsucc (ordsucc n))) ⊆ open_ball X d c (eps_ (pickN c)).
An exact proof term for the current goal is (open_ball_radius_mono X d c (eps_ (ordsucc (ordsucc n))) (eps_ (pickN c)) Hrl).
An exact proof term for the current goal is (Subq_tra (open_ball X d c (eps_ (ordsucc (ordsucc n)))) (open_ball X d c (eps_ (pickN c))) (pickV c) Hmono HsubPick).
We prove the intermediate claim Hcenter_ball_in_V0: ∀c n : set, c ∈ X → n ∈ ω → pickN c ∈ ordsucc (ordsucc n) → ∃v0 : set, v0 ∈ V0 ∧ open_ball X d c (eps_ (ordsucc (ordsucc n))) ⊆ v0.
Let c and n be given.
Assume HcX: c ∈ X.
Assume HnO: n ∈ ω.
Assume HNin: pickN c ∈ ordsucc (ordsucc n).
We use (pickV c) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (pickV c ∈ V0) (∃N : set, N ∈ ω ∧ open_ball X d c (eps_ N) ⊆ pickV c) (HpickV c HcX)).
An exact proof term for the current goal is (Hsmall_ball_in_pickV c n HcX HnO HNin).
Set Eligible to be the term (λn : set ⇒ {c ∈ X|pickN c ∈ ordsucc (ordsucc n)}).
We prove the intermediate claim HEligibleContain: ∀n c : set, n ∈ ω → c ∈ Eligible n → ∃v0 : set, v0 ∈ V0 ∧ open_ball X d c (eps_ (ordsucc (ordsucc n))) ⊆ v0.
Let n and c be given.
Assume HnO: n ∈ ω.
Assume HcEl: c ∈ Eligible n.
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (SepE1 X (λc0 : set ⇒ pickN c0 ∈ ordsucc (ordsucc n)) c HcEl).
We prove the intermediate claim HNin: pickN c ∈ ordsucc (ordsucc n).
An exact proof term for the current goal is (SepE2 X (λc0 : set ⇒ pickN c0 ∈ ordsucc (ordsucc n)) c HcEl).
An exact proof term for the current goal is (Hcenter_ball_in_V0 c n HcX HnO HNin).
We prove the intermediate claim HEligibleCovers: ∀x : set, x ∈ X → ∃n : set, n ∈ ω ∧ x ∈ Eligible n.
Let x be given.
Assume HxX: x ∈ X.
We use (pickN x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (pickN x ∈ ω) (open_ball X d x (eps_ (pickN x)) ⊆ pickV x) (HpickN x HxX)).
We will prove x ∈ Eligible (pickN x).
We prove the intermediate claim Hstep: pickN x ∈ ordsucc (pickN x).
An exact proof term for the current goal is (ordsuccI2 (pickN x)).
We prove the intermediate claim Hstep2: pickN x ∈ ordsucc (ordsucc (pickN x)).
An exact proof term for the current goal is (ordsuccI1 (ordsucc (pickN x)) (pickN x) Hstep).
An exact proof term for the current goal is (SepI X (λc0 : set ⇒ pickN c0 ∈ ordsucc (ordsucc (pickN x))) x HxX Hstep2).
We prove the intermediate claim HexCenters: ∃Centers : set → set, (∀n : set, n ∈ ω → Centers n ⊆ Eligible n) ∧ (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n) ∧ (∀n : set, n ∈ ω → ∀x : set, x ∈ Eligible n → ∃c : set, c ∈ Centers n ∧ x ∈ open_ball X d c (eps_ (ordsucc (ordsucc n)))).
The rest of this subproof is missing.
Apply HexCenters to the current goal.
Let Centers be given.
Assume HCentersPack.
We prove the intermediate claim HCentersAB: (∀n : set, n ∈ ω → Centers n ⊆ Eligible n) ∧ (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n).
An exact proof term for the current goal is (andEL ((∀n : set, n ∈ ω → Centers n ⊆ Eligible n) ∧ (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n)) (∀n : set, n ∈ ω → ∀x : set, x ∈ Eligible n → ∃c : set, c ∈ Centers n ∧ x ∈ open_ball X d c (eps_ (ordsucc (ordsucc n)))) HCentersPack).
We prove the intermediate claim HCentersSub: ∀n : set, n ∈ ω → Centers n ⊆ Eligible n.
An exact proof term for the current goal is (andEL (∀n : set, n ∈ ω → Centers n ⊆ Eligible n) (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n) HCentersAB).
We prove the intermediate claim HCentersSep: ∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n.
An exact proof term for the current goal is (andER (∀n : set, n ∈ ω → Centers n ⊆ Eligible n) (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n) HCentersAB).
We prove the intermediate claim HCentersCover: ∀n : set, n ∈ ω → ∀x : set, x ∈ Eligible n → ∃c : set, c ∈ Centers n ∧ x ∈ open_ball X d c (eps_ (ordsucc (ordsucc n))).
An exact proof term for the current goal is (andER ((∀n : set, n ∈ ω → Centers n ⊆ Eligible n) ∧ (∀n : set, n ∈ ω → eps_separated_set X d (Centers n) n)) (∀n : set, n ∈ ω → ∀x : set, x ∈ Eligible n → ∃c : set, c ∈ Centers n ∧ x ∈ open_ball X d c (eps_ (ordsucc (ordsucc n)))) HCentersPack).
We use Centers to witness the existential quantifier.
Apply andI to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Apply andI to the current goal.
An exact proof term for the current goal is (HCentersSep n HnO).
Let c be given.
Assume HcCn: c ∈ Centers n.
We prove the intermediate claim HcEl: c ∈ Eligible n.
An exact proof term for the current goal is (HCentersSub n HnO c HcCn).
An exact proof term for the current goal is (HEligibleContain n c HnO HcEl).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ x ∈ Eligible n.
An exact proof term for the current goal is (HEligibleCovers x HxX).
Apply Hexn 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 ∈ ω) (x ∈ Eligible n) HnPack).
We prove the intermediate claim HxEl: x ∈ Eligible n.
An exact proof term for the current goal is (andER (n ∈ ω) (x ∈ Eligible n) HnPack).
We prove the intermediate claim Hexc: ∃c : set, c ∈ Centers n ∧ x ∈ open_ball X d c (eps_ (ordsucc (ordsucc n))).
An exact proof term for the current goal is (HCentersCover n HnO x HxEl).
Apply Hexc to the current goal.
Let c be given.
Assume HcPack.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
We use c to witness the existential quantifier.
An exact proof term for the current goal is HcPack.
∎