Let X and d be given.
Assume Hm: metric_on X d.
Set Tx to be the term metric_topology X d.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We will prove sigma_locally_finite_basis X Tx.
We will prove topology_on X Tx ∧ ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Set Bn to be the term (λn : set ⇒ {open_ball X d x (inv_nat (ordsucc n))|x ∈ X}).
Set Vn to be the term (λn : set ⇒ Eps_i (λV : set ⇒ open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn n))).
Set Fams to be the term {Vn n|n ∈ ω}.
We prove the intermediate claim HBnCoverAll: ∀n : set, n ∈ ω → open_cover X Tx (Bn n).
Let n be given.
Assume HnO: n ∈ ω.
We will prove open_cover X Tx (Bn n).
We will prove (∀u : set, u ∈ (Bn n) → u ∈ Tx) ∧ covers X (Bn n).
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ (Bn n).
Apply (ReplE_impred X (λx0 : set ⇒ open_ball X d x0 (inv_nat (ordsucc n))) u Hu (u ∈ Tx)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HuEq: u = open_ball X d x0 (inv_nat (ordsucc n)).
rewrite the current goal using HuEq (from left to right).
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 Hn1NZ: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hn1O.
Assume Hmem0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim Hrpos: Rlt 0 (inv_nat (ordsucc n)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) Hn1NZ).
An exact proof term for the current goal is (open_ball_in_metric_topology X d x0 (inv_nat (ordsucc n)) Hm Hx0X Hrpos).
We will prove covers X (Bn n).
Let x be given.
Assume HxX: x ∈ X.
We use (open_ball X d x (inv_nat (ordsucc n))) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ open_ball X d x0 (inv_nat (ordsucc n))) x HxX).
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 Hn1NZ: ordsucc n ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hn1O.
Assume Hmem0: ordsucc n ∈ {0}.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
We prove the intermediate claim Hrpos: Rlt 0 (inv_nat (ordsucc n)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc n) Hn1NZ).
An exact proof term for the current goal is (center_in_open_ball X d x (inv_nat (ordsucc n)) Hm HxX Hrpos).
We prove the intermediate claim HexVAll: ∀n : set, n ∈ ω → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn n).
Let n be given.
Assume HnO: n ∈ ω.
An exact proof term for the current goal is (metric_fixed_radius_ball_cover_has_locally_finite_refinement X d n Hm HnO).
We use Fams to witness the existential quantifier.
Apply and5I to the current goal.
We prove the intermediate claim HomegaCount: countable_set ω.
An exact proof term for the current goal is omega_countable_set.
An exact proof term for the current goal is (countable_image ω HomegaCount (λn : set ⇒ Vn n)).
We will prove Fams ⊆ 𝒫 (𝒫 X).
Let F be given.
Assume HF: F ∈ Fams.
We will prove F ∈ 𝒫 (𝒫 X).
Apply (ReplE_impred ω (λn0 : set ⇒ Vn n0) F HF (F ∈ 𝒫 (𝒫 X))) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HFdef: F = Vn n.
rewrite the current goal using HFdef (from left to right).
We prove the intermediate claim HBnCover: open_cover X Tx (Bn n).
An exact proof term for the current goal is (HBnCoverAll n HnO).
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn n).
An exact proof term for the current goal is (HexVAll n HnO).
We prove the intermediate claim HVnPack: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n) ∧ refine_of (Vn n) (Bn n).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn n)) HexV).
We prove the intermediate claim HVnCovLf: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n)) (refine_of (Vn n) (Bn n)) HVnPack).
We prove the intermediate claim HVnCover: open_cover X Tx (Vn n).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n)) (locally_finite_family X Tx (Vn n)) HVnCovLf).
We prove the intermediate claim HVnSub: (Vn n) ⊆ 𝒫 X.
An exact proof term for the current goal is (open_cover_family_sub X Tx (Vn n) HTx HVnCover).
An exact proof term for the current goal is (PowerI (𝒫 X) (Vn n) HVnSub).
Let F be given.
Assume HF: F ∈ Fams.
We will prove locally_finite_family X Tx F.
Apply (ReplE_impred ω (λn0 : set ⇒ Vn n0) F HF (locally_finite_family X Tx F)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HFdef: F = Vn n.
rewrite the current goal using HFdef (from left to right).
We prove the intermediate claim HBnCover: open_cover X Tx (Bn n).
An exact proof term for the current goal is (HBnCoverAll n HnO).
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn n).
An exact proof term for the current goal is (HexVAll n HnO).
We prove the intermediate claim HVnPack: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n) ∧ refine_of (Vn n) (Bn n).
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn n)) HexV).
We prove the intermediate claim HVnCovLf: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n)) (refine_of (Vn n) (Bn n)) HVnPack).
An exact proof term for the current goal is (andER (open_cover X Tx (Vn n)) (locally_finite_family X Tx (Vn n)) HVnCovLf).
We prove the intermediate claim HBopen: ∀c ∈ ⋃ Fams, c ∈ Tx.
Let c be given.
Assume HcUF: c ∈ ⋃ Fams.
Apply (UnionE_impred Fams c HcUF (c ∈ Tx)) to the current goal.
Let V be given.
Assume HcV: c ∈ V.
Assume HVF: V ∈ Fams.
Apply (ReplE_impred ω (λn0 : set ⇒ Vn n0) V HVF (c ∈ Tx)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HVdef: V = Vn n.
We prove the intermediate claim HcVn: c ∈ Vn n.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HcV.
We prove the intermediate claim HBnCover: open_cover X Tx (Bn n).
An exact proof term for the current goal is (HBnCoverAll n HnO).
We prove the intermediate claim HexV: ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 (Bn n).
An exact proof term for the current goal is (HexVAll n HnO).
We prove the intermediate claim HVnPack: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n) ∧ refine_of (Vn n) (Bn n).
An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 (Bn n)) HexV).
We prove the intermediate claim HVnCover: open_cover X Tx (Vn n).
We prove the intermediate claim HVnCovLf: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n)) (refine_of (Vn n) (Bn n)) HVnPack).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n)) (locally_finite_family X Tx (Vn n)) HVnCovLf).
An exact proof term for the current goal is (open_cover_members_open X Tx (Vn n) c HVnCover HcVn).
We prove the intermediate claim Hlocal: ∀U ∈ Tx, ∀x ∈ U, ∃Cx ∈ ⋃ Fams, x ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ Tx.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HUgen: U ∈ generated_topology X (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r})).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUcond: ∀y ∈ U, ∃b0 ∈ (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r})), y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y : set, y ∈ U0 → ∃b0 ∈ (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r})), y ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb0: ∃b0 ∈ (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r})), x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUcond x HxU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B: b0 ∈ (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r})).
An exact proof term for the current goal is (andEL (b0 ∈ (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}))) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ (famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}))) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0prop).
Apply (famunionE_impred X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}) b0 Hb0B (∃Cx ∈ ⋃ Fams, x ∈ Cx ∧ Cx ⊆ U)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hb0In: b0 ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b0 Hb0In (∃Cx ∈ ⋃ Fams, x ∈ Cx ∧ Cx ⊆ U)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hb0eq: b0 = open_ball X d c r0.
We prove the intermediate claim HxinBall: x ∈ open_ball X d c r0.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (open_ballE1 X d c r0 x HxinBall).
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ Rlt 0 r ∧ open_ball X d x r ⊆ open_ball X d c r0.
An exact proof term for the current goal is (open_ball_refine_center X d c x r0 Hm HcX HxX Hr0R Hr0pos HxinBall).
Apply Hexr to the current goal.
Let r be given.
Assume HrPack: r ∈ R ∧ Rlt 0 r ∧ open_ball X d x r ⊆ open_ball X d c r0.
We prove the intermediate claim Hr12: r ∈ R ∧ Rlt 0 r.
An exact proof term for the current goal is (andEL (r ∈ R ∧ Rlt 0 r) (open_ball X d x r ⊆ open_ball X d c r0) HrPack).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r) Hr12).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r) Hr12).
We prove the intermediate claim HballSub: open_ball X d x r ⊆ open_ball X d c r0.
An exact proof term for the current goal is (andER (r ∈ R ∧ Rlt 0 r) (open_ball X d x r ⊆ open_ball X d c r0) HrPack).
We prove the intermediate claim HballSubU: open_ball X d x r ⊆ U.
We prove the intermediate claim Hball2: open_ball X d c r0 ⊆ U.
Let t be given.
Assume HtBall: t ∈ open_ball X d c r0.
We will prove t ∈ U.
We prove the intermediate claim HtB0: t ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HtBall.
An exact proof term for the current goal is (Hb0subU t HtB0).
An exact proof term for the current goal is (Subq_tra (open_ball X d x r) (open_ball X d c r0) U HballSub Hball2).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim He1R: eps_ 1 ∈ R.
An exact proof term for the current goal is (RltE_right 0 (eps_ 1) eps_1_pos_R).
We prove the intermediate claim He1Real: eps_ 1 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is He1R.
We prove the intermediate claim HrReal: r ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HrR.
We prove the intermediate claim HrhalfReal: mul_SNo (eps_ 1) r ∈ real.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) He1Real r HrReal).
We prove the intermediate claim HrhalfR: mul_SNo (eps_ 1) r ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is HrhalfReal.
We prove the intermediate claim He1S: SNo (eps_ 1).
An exact proof term for the current goal is SNo_eps_1.
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HrhalfS: SNo (mul_SNo (eps_ 1) r).
An exact proof term for the current goal is (SNo_mul_SNo (eps_ 1) r He1S HrS).
We prove the intermediate claim He1posS: 0 < (eps_ 1).
An exact proof term for the current goal is (RltE_lt 0 (eps_ 1) eps_1_pos_R).
We prove the intermediate claim HrposS: 0 < r.
An exact proof term for the current goal is (RltE_lt 0 r Hrpos).
We prove the intermediate claim HrhalfPosS: 0 < mul_SNo (eps_ 1) r.
An exact proof term for the current goal is (mul_SNo_pos_pos (eps_ 1) r He1S HrS He1posS HrposS).
We prove the intermediate claim HrhalfPos: Rlt 0 (mul_SNo (eps_ 1) r).
An exact proof term for the current goal is (RltI 0 (mul_SNo (eps_ 1) r) real_0 HrhalfR HrhalfPosS).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r).
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt (mul_SNo (eps_ 1) r) HrhalfR HrhalfPos).
Apply HexN to the current goal.
Let N be given.
Assume HNpack: N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r).
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r)) HNpack).
We prove the intermediate claim HinvLtHalf: Rlt (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r).
An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r)) HNpack).
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 HN1NZ: ordsucc N ∈ ω ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HN1O.
Assume Hmem0: ordsucc N ∈ {0}.
We prove the intermediate claim Heq0: ordsucc N = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc N) Hmem0).
An exact proof term for the current goal is (neq_ordsucc_0 N Heq0).
We prove the intermediate claim HinvR: inv_nat (ordsucc N) ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc N) HN1O).
We prove the intermediate claim HinvPos: Rlt 0 (inv_nat (ordsucc N)).
An exact proof term for the current goal is (inv_nat_pos (ordsucc N) HN1NZ).
We prove the intermediate claim H2invLt: Rlt (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))) (add_SNo (mul_SNo (eps_ 1) r) (mul_SNo (eps_ 1) r)).
An exact proof term for the current goal is (Rlt_add_SNo (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r) (inv_nat (ordsucc N)) (mul_SNo (eps_ 1) r) HinvLtHalf HinvLtHalf).
We prove the intermediate claim HhalfSumEq: add_SNo (mul_SNo (eps_ 1) r) (mul_SNo (eps_ 1) r) = r.
rewrite the current goal using (mul_SNo_distrR (eps_ 1) (eps_ 1) r He1S He1S HrS) (from right to left).
rewrite the current goal using eps_1_half_eq1 (from left to right).
An exact proof term for the current goal is (mul_SNo_oneL r HrS).
We prove the intermediate claim H2invLtR: Rlt (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))) r.
rewrite the current goal using HhalfSumEq (from right to left).
An exact proof term for the current goal is H2invLt.
Set V to be the term Vn N.
We prove the intermediate claim HBnCover: open_cover X Tx (Bn N).
An exact proof term for the current goal is (HBnCoverAll N HNO).
We prove the intermediate claim HexV: ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 (Bn N).
An exact proof term for the current goal is (HexVAll N HNO).
We prove the intermediate claim HVpack: open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V (Bn N).
An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 (Bn N)) HexV).
We prove the intermediate claim HVcovLf: open_cover X Tx V ∧ locally_finite_family X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V (Bn N)) HVpack).
We prove the intermediate claim HVcover: open_cover X Tx V.
An exact proof term for the current goal is (andEL (open_cover X Tx V) (locally_finite_family X Tx V) HVcovLf).
We prove the intermediate claim HVref: refine_of V (Bn N).
An exact proof term for the current goal is (andER (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V (Bn N)) HVpack).
We prove the intermediate claim Hexv: ∃v : set, v ∈ V ∧ x ∈ v.
We prove the intermediate claim HVcovers: covers X V.
An exact proof term for the current goal is (open_cover_implies_covers X Tx V HVcover).
An exact proof term for the current goal is (HVcovers x HxX).
Apply Hexv to the current goal.
Let v be given.
Assume Hvpair: v ∈ V ∧ x ∈ v.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (v ∈ V) (x ∈ v) Hvpair).
We prove the intermediate claim Hxv: x ∈ v.
An exact proof term for the current goal is (andER (v ∈ V) (x ∈ v) Hvpair).
Apply (HVref v HvV) to the current goal.
Let u be given.
Assume Hupair: u ∈ (Bn N) ∧ v ⊆ u.
We prove the intermediate claim HuBn: u ∈ (Bn N).
An exact proof term for the current goal is (andEL (u ∈ (Bn N)) (v ⊆ u) Hupair).
We prove the intermediate claim Hvsubu: v ⊆ u.
An exact proof term for the current goal is (andER (u ∈ (Bn N)) (v ⊆ u) Hupair).
We prove the intermediate claim Hxu: x ∈ u.
An exact proof term for the current goal is (Hvsubu x Hxv).
Apply (ReplE_impred X (λc0 : set ⇒ open_ball X d c0 (inv_nat (ordsucc N))) u HuBn (∃Cx ∈ ⋃ Fams, x ∈ Cx ∧ Cx ⊆ U)) to the current goal.
Let c0 be given.
Assume Hc0X: c0 ∈ X.
Assume HuEq: u = open_ball X d c0 (inv_nat (ordsucc N)).
We prove the intermediate claim HxuBall: x ∈ open_ball X d c0 (inv_nat (ordsucc N)).
rewrite the current goal using HuEq (from right to left).
An exact proof term for the current goal is Hxu.
We prove the intermediate claim Hc0In: c0 ∈ open_ball X d x (inv_nat (ordsucc N)).
We prove the intermediate claim Hlt_c0x: Rlt (apply_fun d (c0,x)) (inv_nat (ordsucc N)).
An exact proof term for the current goal is (open_ballE2 X d c0 (inv_nat (ordsucc N)) x HxuBall).
We prove the intermediate claim Hlt_xc0: Rlt (apply_fun d (x,c0)) (inv_nat (ordsucc N)).
rewrite the current goal using (metric_on_symmetric X d x c0 Hm HxX Hc0X) (from left to right).
An exact proof term for the current goal is Hlt_c0x.
An exact proof term for the current goal is (open_ballI X d x (inv_nat (ordsucc N)) c0 Hc0X Hlt_xc0).
We prove the intermediate claim HuSubBall: u ⊆ open_ball X d x (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))).
Let y be given.
Assume Hyu: y ∈ u.
We prove the intermediate claim HyuBall: y ∈ open_ball X d c0 (inv_nat (ordsucc N)).
rewrite the current goal using HuEq (from right to left).
An exact proof term for the current goal is Hyu.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d c0 (inv_nat (ordsucc N)) y HyuBall).
We prove the intermediate claim Hc0InY: c0 ∈ open_ball X d y (inv_nat (ordsucc N)).
We prove the intermediate claim HyLt_c0y: Rlt (apply_fun d (c0,y)) (inv_nat (ordsucc N)).
An exact proof term for the current goal is (open_ballE2 X d c0 (inv_nat (ordsucc N)) y HyuBall).
We prove the intermediate claim HyLt_yc0: Rlt (apply_fun d (y,c0)) (inv_nat (ordsucc N)).
rewrite the current goal using (metric_on_symmetric X d y c0 Hm HyX Hc0X) (from left to right).
An exact proof term for the current goal is HyLt_c0y.
An exact proof term for the current goal is (open_ballI X d y (inv_nat (ordsucc N)) c0 Hc0X HyLt_yc0).
We prove the intermediate claim Hdlt: Rlt (apply_fun d (x,y)) (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))).
An exact proof term for the current goal is (metric_ball_intersect_centers_lt_add X d x y c0 (inv_nat (ordsucc N)) (inv_nat (ordsucc N)) Hm HxX HyX Hc0X HinvR HinvR Hc0In Hc0InY).
An exact proof term for the current goal is (open_ballI X d x (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))) y HyX Hdlt).
We prove the intermediate claim HballMono: open_ball X d x (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))) ⊆ open_ball X d x r.
An exact proof term for the current goal is (open_ball_radius_mono X d x (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N))) r H2invLtR).
We prove the intermediate claim HuSubU: u ⊆ U.
An exact proof term for the current goal is (Subq_tra u (open_ball X d x r) U (Subq_tra u (open_ball X d x (add_SNo (inv_nat (ordsucc N)) (inv_nat (ordsucc N)))) (open_ball X d x r) HuSubBall HballMono) HballSubU).
We use v to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HVFams: V ∈ Fams.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ Vn n0) N HNO).
An exact proof term for the current goal is (UnionI Fams v V HvV HVFams).
Apply andI to the current goal.
An exact proof term for the current goal is Hxv.
An exact proof term for the current goal is (Subq_tra v u U Hvsubu HuSubU).
We prove the intermediate claim HBasisGen: basis_on X (⋃ Fams) ∧ generated_topology X (⋃ Fams) = Tx.
An exact proof term for the current goal is (basis_refines_topology X Tx (⋃ Fams) HTx HBopen Hlocal).
An exact proof term for the current goal is HBasisGen.
Let b be given.
Assume HbUF: b ∈ ⋃ Fams.
We will prove b ∈ Tx.
Apply (UnionE_impred Fams b HbUF (b ∈ Tx)) to the current goal.
Let V be given.
Assume HbV: b ∈ V.
Assume HVF: V ∈ Fams.
Apply (ReplE_impred ω (λn0 : set ⇒ Vn n0) V HVF (b ∈ Tx)) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HVdef: V = Vn n.
We prove the intermediate claim HbVn: b ∈ Vn n.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HbV.
We prove the intermediate claim HBnCover: open_cover X Tx (Bn n).
An exact proof term for the current goal is (HBnCoverAll n HnO).
We prove the intermediate claim HexV: ∃V0 : set, open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 (Bn n).
An exact proof term for the current goal is (HexVAll n HnO).
We prove the intermediate claim HVnPack: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n) ∧ refine_of (Vn n) (Bn n).
An exact proof term for the current goal is (Eps_i_ex (λV0 : set ⇒ open_cover X Tx V0 ∧ locally_finite_family X Tx V0 ∧ refine_of V0 (Bn n)) HexV).
We prove the intermediate claim HVnCovLf: open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n) ∧ locally_finite_family X Tx (Vn n)) (refine_of (Vn n) (Bn n)) HVnPack).
We prove the intermediate claim HVnCover: open_cover X Tx (Vn n).
An exact proof term for the current goal is (andEL (open_cover X Tx (Vn n)) (locally_finite_family X Tx (Vn n)) HVnCovLf).
An exact proof term for the current goal is (open_cover_members_open X Tx (Vn n) b HVnCover HbVn).
∎