Let x and r be given.
Assume Hm: metric_on R_omega_space Romega_D_metric.
Assume Hx: x ∈ R_omega_space.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Set Xi0 to be the term const_space_family ω R R_standard_topology.
Set S to be the term product_subbasis_full ω Xi0.
We prove the intermediate claim Hdef: R_omega_product_topology = generated_topology_from_subbasis R_omega_space S.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Set X to be the term R_omega_space.
Set d to be the term Romega_D_metric.
Set B to be the term basis_of_subbasis X S.
We prove the intermediate claim HTdef: generated_topology_from_subbasis X S = generated_topology X B.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We prove the intermediate claim Hgendef: generated_topology X B = {U0 ∈ 𝒫 X|∀y ∈ U0, ∃b ∈ B, y ∈ b ∧ b ⊆ U0}.
Use reflexivity.
rewrite the current goal using Hgendef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is (PowerI X (open_ball X d x r) (open_ball_subset_X X d x r)).
Let y be given.
Assume Hy: y ∈ open_ball X d x r.
We will prove ∃b ∈ B, y ∈ b ∧ b ⊆ open_ball X d x r.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x r y Hy).
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y Hx HyX).
We prove the intermediate claim Hdapp: apply_fun d (x,y) = Romega_D_metric_value x y.
rewrite the current goal using (apply_fun_graph (setprod X X) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
We prove the intermediate claim Hltball: Rlt (apply_fun d (x,y)) r.
An exact proof term for the current goal is (open_ballE2 X d x r y Hy).
We prove the intermediate claim Hltval: Rlt (Romega_D_metric_value x y) r.
rewrite the current goal using Hdapp (from right to left).
An exact proof term for the current goal is Hltball.
We prove the intermediate claim HexF: ∃F : set, (F ∈ finite_subcollections S ∧ y ∈ intersection_of_family X F) ∧ intersection_of_family X F ⊆ open_ball X d x r.
Set dxy to be the term apply_fun d (x,y).
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hm).
We prove the intermediate claim HdxyR: dxy ∈ R.
An exact proof term for the current goal is (Hfun (x,y) Hxyprod).
We prove the intermediate claim HdxyS: SNo dxy.
An exact proof term for the current goal is (real_SNo dxy HdxyR).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
Set gap to be the term add_SNo r (minus_SNo dxy).
We prove the intermediate claim HgapR: gap ∈ R.
An exact proof term for the current goal is (real_add_SNo r HrR (minus_SNo dxy) (real_minus_SNo dxy HdxyR)).
We prove the intermediate claim HgapPos: Rlt 0 gap.
We prove the intermediate claim HmdxyS: SNo (minus_SNo dxy).
An exact proof term for the current goal is (SNo_minus_SNo dxy HdxyS).
We prove the intermediate claim HdxyltS: dxy < r.
An exact proof term for the current goal is (RltE_lt dxy r Hltball).
We prove the intermediate claim Hlt': add_SNo (minus_SNo dxy) dxy < add_SNo (minus_SNo dxy) r.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo dxy) dxy r HmdxyS HdxyS HrS HdxyltS).
We prove the intermediate claim H0eq: add_SNo (minus_SNo dxy) dxy = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv dxy HdxyS).
We prove the intermediate claim Hcom: add_SNo (minus_SNo dxy) r = gap.
We prove the intermediate claim Hcom0: add_SNo (minus_SNo dxy) r = add_SNo r (minus_SNo dxy).
An exact proof term for the current goal is (add_SNo_com (minus_SNo dxy) r HmdxyS HrS).
rewrite the current goal using Hcom0 (from left to right).
Use reflexivity.
We prove the intermediate claim HgapPosS: 0 < gap.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is Hlt'.
An exact proof term for the current goal is (RltI 0 gap real_0 HgapR HgapPosS).
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim H1pos: Rlt 0 1.
An exact proof term for the current goal is Rlt_0_1.
We prove the intermediate claim Hexeps: ∃eps : set, eps ∈ R ∧ Rlt 0 eps ∧ Rlt eps gap ∧ Rlt eps 1 ∧ Rlt eps 1 ∧ Rlt eps 1.
An exact proof term for the current goal is (exists_eps_lt_four_pos_Euclid gap 1 1 1 HgapR H1R H1R H1R HgapPos H1pos H1pos H1pos).
Apply Hexeps to the current goal.
Let eps be given.
Assume Hepsconj.
We prove the intermediate claim HepsTop: ((((eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps gap) ∧ Rlt eps 1) ∧ Rlt eps 1) ∧ Rlt eps 1.
An exact proof term for the current goal is Hepsconj.
We prove the intermediate claim HepsTop1: (((eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps gap) ∧ Rlt eps 1) ∧ Rlt eps 1.
Apply HepsTop to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H1.
We prove the intermediate claim HepsTop2: ((eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps gap) ∧ Rlt eps 1.
Apply HepsTop1 to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H1.
We prove the intermediate claim HepsTop3: (eps ∈ R ∧ Rlt 0 eps) ∧ Rlt eps gap.
Apply HepsTop2 to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H1.
We prove the intermediate claim HepsPair: eps ∈ R ∧ Rlt 0 eps.
Apply HepsTop3 to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H1.
We prove the intermediate claim HepsR: eps ∈ R.
Apply HepsPair to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H1.
We prove the intermediate claim HepsPos: Rlt 0 eps.
Apply HepsPair to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H2.
We prove the intermediate claim HepsLtGap: Rlt eps gap.
Apply HepsTop3 to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H2.
We prove the intermediate claim HepsLt1: Rlt eps 1.
Apply HepsTop2 to the current goal.
Assume H1 H2.
An exact proof term for the current goal is H2.
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) eps.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt eps HepsR HepsPos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) eps) HNpair).
We prove the intermediate claim HinvNLt: Rlt (inv_nat (ordsucc N)) eps.
An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) eps) HNpair).
Set I to be the term ordsucc N.
We prove the intermediate claim HIO: I ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNO).
We prove the intermediate claim HIcOmega: I ⊆ ω.
An exact proof term for the current goal is (ordinal_ordsucc_In_Subq ω omega_ordinal N HNO).
Set cyl to be the term (λi : set ⇒ product_cylinder ω Xi0 i (open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps))).
Set F to be the term Repl I cyl.
We use F to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HFdef: finite_subcollections S = {F0 ∈ 𝒫 S|finite F0}.
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let s be given.
Assume HsF: s ∈ F.
We will prove s ∈ S.
We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ s = cyl i.
An exact proof term for the current goal is (ReplE I cyl s HsF).
Apply Hexi to the current goal.
Let i be given.
Assume Hiconj.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (s = cyl i) Hiconj).
We prove the intermediate claim Hseq: s = cyl i.
An exact proof term for the current goal is (andER (i ∈ I) (s = cyl i) Hiconj).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (HIcOmega i HiI).
Set Ui to be the term open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps).
We prove the intermediate claim HUiTop: Ui ∈ R_standard_topology.
We prove the intermediate claim HyiR: apply_fun y i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i HyX HiO).
We prove the intermediate claim HyiS: SNo (apply_fun y i).
An exact proof term for the current goal is (real_SNo (apply_fun y i) HyiR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HmeiR: minus_SNo eps ∈ R.
An exact proof term for the current goal is (real_minus_SNo eps HepsR).
We prove the intermediate claim HaR: add_SNo (apply_fun y i) (minus_SNo eps) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun y i) HyiR (minus_SNo eps) HmeiR).
We prove the intermediate claim HbR: add_SNo (apply_fun y i) eps ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun y i) HyiR eps HepsR).
We prove the intermediate claim HbStd: Ui ∈ R_standard_basis.
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) (add_SNo (apply_fun y i) (minus_SNo eps)) Ui HaR (ReplI R (λb1 : set ⇒ open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) b1) (add_SNo (apply_fun y i) eps) HbR)).
We prove the intermediate claim HPow: Ui ∈ 𝒫 R.
We prove the intermediate claim HUiEq: Ui = open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps).
Use reflexivity.
rewrite the current goal using HUiEq (from left to right).
An exact proof term for the current goal is (PowerI R (open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps)) (open_interval_Subq_R (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps))).
An exact proof term for the current goal is (generated_topology_contains_elem R R_standard_basis Ui HPow HbStd).
We prove the intermediate claim HcylIn: product_cylinder ω Xi0 i Ui ∈ S.
We prove the intermediate claim HTi: space_family_topology Xi0 i = R_standard_topology.
We prove the intermediate claim Hdef0: space_family_topology Xi0 i = (apply_fun Xi0 i) 1.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (const_space_family_apply ω R R_standard_topology i HiO) (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
We prove the intermediate claim HUiIn: Ui ∈ space_family_topology Xi0 i.
rewrite the current goal using HTi (from left to right).
An exact proof term for the current goal is HUiTop.
An exact proof term for the current goal is (famunionI ω (λj : set ⇒ {product_cylinder ω Xi0 j U0|U0 ∈ space_family_topology Xi0 j}) i (product_cylinder ω Xi0 i Ui) HiO (ReplI (space_family_topology Xi0 i) (λU0 : set ⇒ product_cylinder ω Xi0 i U0) Ui HUiIn)).
An exact proof term for the current goal is HcylIn.
We prove the intermediate claim HINat: nat_p I.
An exact proof term for the current goal is (omega_nat_p I HIO).
We prove the intermediate claim HIfin: finite I.
An exact proof term for the current goal is (nat_finite I HINat).
An exact proof term for the current goal is (Repl_finite cyl I HIfin).
We prove the intermediate claim HinterDef: intersection_of_family X F = {x0 ∈ X|∀U : set, U ∈ F → x0 ∈ U}.
Use reflexivity.
rewrite the current goal using HinterDef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
Let U0 be given.
Assume HU0: U0 ∈ F.
We will prove y ∈ U0.
We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ U0 = cyl i.
An exact proof term for the current goal is (ReplE I cyl U0 HU0).
Apply Hexi to the current goal.
Let i be given.
Assume Hiconj.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (U0 = cyl i) Hiconj).
We prove the intermediate claim HU0eq: U0 = cyl i.
An exact proof term for the current goal is (andER (i ∈ I) (U0 = cyl i) Hiconj).
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (HIcOmega i HiI).
Set Ui to be the term open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps).
We prove the intermediate claim HCdef: cyl i = {f0 ∈ product_space ω Xi0|i ∈ ω ∧ Ui ∈ space_family_topology Xi0 i ∧ apply_fun f0 i ∈ Ui}.
Use reflexivity.
rewrite the current goal using HCdef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
We will prove i ∈ ω ∧ Ui ∈ space_family_topology Xi0 i ∧ apply_fun y i ∈ Ui.
We prove the intermediate claim HUiTop: Ui ∈ R_standard_topology.
We prove the intermediate claim HyiR: apply_fun y i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i HyX HiO).
We prove the intermediate claim HmeiR: minus_SNo eps ∈ R.
An exact proof term for the current goal is (real_minus_SNo eps HepsR).
We prove the intermediate claim HaR: add_SNo (apply_fun y i) (minus_SNo eps) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun y i) HyiR (minus_SNo eps) HmeiR).
We prove the intermediate claim HbR: add_SNo (apply_fun y i) eps ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun y i) HyiR eps HepsR).
We prove the intermediate claim HbStd: Ui ∈ R_standard_basis.
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) (add_SNo (apply_fun y i) (minus_SNo eps)) Ui HaR (ReplI R (λb1 : set ⇒ open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) b1) (add_SNo (apply_fun y i) eps) HbR)).
We prove the intermediate claim HPow: Ui ∈ 𝒫 R.
We prove the intermediate claim HUiEq: Ui = open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps).
Use reflexivity.
rewrite the current goal using HUiEq (from left to right).
An exact proof term for the current goal is (PowerI R (open_interval (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps)) (open_interval_Subq_R (add_SNo (apply_fun y i) (minus_SNo eps)) (add_SNo (apply_fun y i) eps))).
An exact proof term for the current goal is (generated_topology_contains_elem R R_standard_basis Ui HPow HbStd).
We prove the intermediate claim HTi: space_family_topology Xi0 i = R_standard_topology.
We prove the intermediate claim Hdef0: space_family_topology Xi0 i = (apply_fun Xi0 i) 1.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (const_space_family_apply ω R R_standard_topology i HiO) (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
We prove the intermediate claim HUiIn: Ui ∈ space_family_topology Xi0 i.
rewrite the current goal using HTi (from left to right).
An exact proof term for the current goal is HUiTop.
We prove the intermediate claim HyUi: apply_fun y i ∈ Ui.
We prove the intermediate claim HyiR: apply_fun y i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i HyX HiO).
We prove the intermediate claim HyiS: SNo (apply_fun y i).
An exact proof term for the current goal is (real_SNo (apply_fun y i) HyiR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HmepsS: SNo (minus_SNo eps).
An exact proof term for the current goal is (SNo_minus_SNo eps HepsS).
We prove the intermediate claim Hlt1: add_SNo (apply_fun y i) (minus_SNo eps) < apply_fun y i.
rewrite the current goal using (add_SNo_0R (apply_fun y i) HyiS) (from right to left) at position 2.
We prove the intermediate claim HepsPosS: 0 < eps.
An exact proof term for the current goal is (RltE_lt 0 eps HepsPos).
We prove the intermediate claim HepsNegS: minus_SNo eps < 0.
We prove the intermediate claim Htmp: minus_SNo eps < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 eps SNo_0 HepsS HepsPosS).
We prove the intermediate claim Htmp2: minus_SNo eps < 0.
rewrite the current goal using minus_SNo_0 (from right to left).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Htmp2.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun y i) (minus_SNo eps) 0 HyiS HmepsS SNo_0 HepsNegS).
We prove the intermediate claim Hlt2: apply_fun y i < add_SNo (apply_fun y i) eps.
rewrite the current goal using (add_SNo_0R (apply_fun y i) HyiS) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun y i) 0 eps HyiS SNo_0 HepsS (RltE_lt 0 eps HepsPos)).
We prove the intermediate claim Hlt1R: Rlt (add_SNo (apply_fun y i) (minus_SNo eps)) (apply_fun y i).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun y i) (minus_SNo eps)) (apply_fun y i) (real_add_SNo (apply_fun y i) HyiR (minus_SNo eps) (real_minus_SNo eps HepsR)) HyiR Hlt1).
We prove the intermediate claim Hlt2R: Rlt (apply_fun y i) (add_SNo (apply_fun y i) eps).
An exact proof term for the current goal is (RltI (apply_fun y i) (add_SNo (apply_fun y i) eps) HyiR (real_add_SNo (apply_fun y i) HyiR eps HepsR) Hlt2).
We prove the intermediate claim HinterDef: Ui = {x0 ∈ R|Rlt (add_SNo (apply_fun y i) (minus_SNo eps)) x0 ∧ Rlt x0 (add_SNo (apply_fun y i) eps)}.
Use reflexivity.
rewrite the current goal using HinterDef (from left to right).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (add_SNo (apply_fun y i) (minus_SNo eps)) x0 ∧ Rlt x0 (add_SNo (apply_fun y i) eps)) (apply_fun y i) HyiR (andI (Rlt (add_SNo (apply_fun y i) (minus_SNo eps)) (apply_fun y i)) (Rlt (apply_fun y i) (add_SNo (apply_fun y i) eps)) Hlt1R Hlt2R)).
We prove the intermediate claim Hleft: i ∈ ω ∧ Ui ∈ space_family_topology Xi0 i.
An exact proof term for the current goal is (andI (i ∈ ω) (Ui ∈ space_family_topology Xi0 i) HiO HUiIn).
An exact proof term for the current goal is (andI (i ∈ ω ∧ Ui ∈ space_family_topology Xi0 i) (apply_fun y i ∈ Ui) Hleft HyUi).
We will prove intersection_of_family X F ⊆ open_ball X d x r.
Let z be given.
Assume HzInt: z ∈ intersection_of_family X F.
We will prove z ∈ open_ball X d x r.
We prove the intermediate claim HinterDefZ: intersection_of_family X F = {x0 ∈ X|∀U : set, U ∈ F → x0 ∈ U}.
Use reflexivity.
We prove the intermediate claim HzInt0: z ∈ {x0 ∈ X|∀U : set, U ∈ F → x0 ∈ U}.
rewrite the current goal using HinterDefZ (from right to left).
An exact proof term for the current goal is HzInt.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ F → x0 ∈ U) z HzInt0).
We prove the intermediate claim HzAll: ∀U : set, U ∈ F → z ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ F → x0 ∈ U) z HzInt0).
We prove the intermediate claim Htri: Rle (apply_fun d (x,z)) (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))).
An exact proof term for the current goal is (metric_triangle_Rle X d x y z Hm Hx HyX HzX).
We prove the intermediate claim Hyzprod: (y,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y z HyX HzX).
We prove the intermediate claim Hxyprod2: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y Hx HyX).
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hm).
We prove the intermediate claim HdxyR: apply_fun d (x,y) ∈ R.
An exact proof term for the current goal is (Hfun (x,y) Hxyprod2).
We prove the intermediate claim HdyzR: apply_fun d (y,z) ∈ R.
An exact proof term for the current goal is (Hfun (y,z) Hyzprod).
We prove the intermediate claim HdxyEq: apply_fun d (x,y) = Romega_D_metric_value x y.
rewrite the current goal using (apply_fun_graph (setprod X X) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,y) Hxyprod2) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
We prove the intermediate claim HdyzEq: apply_fun d (y,z) = Romega_D_metric_value y z.
rewrite the current goal using (apply_fun_graph (setprod X X) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (y,z) Hyzprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
Use reflexivity.
We prove the intermediate claim HdyzLe: Rle (apply_fun d (y,z)) eps.
rewrite the current goal using HdyzEq (from left to right).
Set A to be the term Romega_D_scaled_diffs y z.
Set l to be the term Romega_D_metric_value y z.
We prove the intermediate claim Hlub: R_lub A l.
An exact proof term for the current goal is (Romega_D_metric_value_is_lub y z HyX HzX).
We prove the intermediate claim HlubCore: l ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a l.
An exact proof term for the current goal is (andEL (l ∈ R ∧ (∀a : set, a ∈ A → a ∈ R → Rle a l)) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim HlubMin: ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u.
An exact proof term for the current goal is (andER (l ∈ R ∧ (∀a : set, a ∈ A → a ∈ R → Rle a l)) (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u) Hlub).
We prove the intermediate claim Hub: ∀a : set, a ∈ A → a ∈ R → Rle a eps.
Let a be given.
Assume HaA: a ∈ A.
Assume HaR: a ∈ R.
Apply (ReplE_impred ω (λi0 : set ⇒ mul_SNo (R_bounded_distance (apply_fun y i0) (apply_fun z i0)) (inv_nat (ordsucc i0))) a HaA (Rle a eps)) to the current goal.
Let i0 be given.
Assume Hi0O: i0 ∈ ω.
Assume Hai0: a = mul_SNo (R_bounded_distance (apply_fun y i0) (apply_fun z i0)) (inv_nat (ordsucc i0)).
rewrite the current goal using Hai0 (from left to right).
Apply (xm (i0 ∈ I)) to the current goal.
Assume Hi0I: i0 ∈ I.
Set yi to be the term apply_fun y i0.
Set zi to be the term apply_fun z i0.
Set Ui0 to be the term open_interval (add_SNo yi (minus_SNo eps)) (add_SNo yi eps).
Set bd to be the term R_bounded_distance yi zi.
Set inv to be the term inv_nat (ordsucc i0).
We prove the intermediate claim HyiR: yi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i0 HyX Hi0O).
We prove the intermediate claim HziR: zi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R z i0 HzX Hi0O).
We prove the intermediate claim HyiS: SNo yi.
An exact proof term for the current goal is (real_SNo yi HyiR).
We prove the intermediate claim HziS: SNo zi.
An exact proof term for the current goal is (real_SNo zi HziR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HbdR: bd ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R yi zi HyiR HziR).
We prove the intermediate claim HbdS: SNo bd.
An exact proof term for the current goal is (real_SNo bd HbdR).
We prove the intermediate claim HSi0: ordsucc i0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i0 Hi0O).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i0) HSi0).
We prove the intermediate claim HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HmulR: mul_SNo bd inv ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd HbdR inv HinvR).
We prove the intermediate claim HmulS: SNo (mul_SNo bd inv).
An exact proof term for the current goal is (real_SNo (mul_SNo bd inv) HmulR).
We prove the intermediate claim HcylInF: cyl i0 ∈ F.
We prove the intermediate claim HFdef: F = Repl I cyl.
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (ReplI I cyl i0 Hi0I).
We prove the intermediate claim HzCyl: z ∈ cyl i0.
An exact proof term for the current goal is (HzAll (cyl i0) HcylInF).
We prove the intermediate claim HzCyl0: z ∈ product_cylinder ω Xi0 i0 Ui0.
We will prove z ∈ product_cylinder ω Xi0 i0 Ui0.
We prove the intermediate claim HcylEq: cyl i0 = product_cylinder ω Xi0 i0 Ui0.
Use reflexivity.
rewrite the current goal using HcylEq (from right to left).
An exact proof term for the current goal is HzCyl.
We prove the intermediate claim HzCylConj: i0 ∈ ω ∧ Ui0 ∈ space_family_topology Xi0 i0 ∧ apply_fun z i0 ∈ Ui0.
An exact proof term for the current goal is (SepE2 (product_space ω Xi0) (λf0 : set ⇒ i0 ∈ ω ∧ Ui0 ∈ space_family_topology Xi0 i0 ∧ apply_fun f0 i0 ∈ Ui0) z HzCyl0).
We prove the intermediate claim HziUi0: zi ∈ Ui0.
Apply HzCylConj to the current goal.
Assume Htmp HziUi0.
An exact proof term for the current goal is HziUi0.
We prove the intermediate claim HUi0Def: Ui0 = {x0 ∈ R|Rlt (add_SNo yi (minus_SNo eps)) x0 ∧ Rlt x0 (add_SNo yi eps)}.
Use reflexivity.
We prove the intermediate claim HziUi0': zi ∈ {x0 ∈ R|Rlt (add_SNo yi (minus_SNo eps)) x0 ∧ Rlt x0 (add_SNo yi eps)}.
rewrite the current goal using HUi0Def (from right to left).
An exact proof term for the current goal is HziUi0.
We prove the intermediate claim HziConj: Rlt (add_SNo yi (minus_SNo eps)) zi ∧ Rlt zi (add_SNo yi eps).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (add_SNo yi (minus_SNo eps)) x0 ∧ Rlt x0 (add_SNo yi eps)) zi HziUi0').
We prove the intermediate claim HleftR: Rlt (add_SNo yi (minus_SNo eps)) zi.
An exact proof term for the current goal is (andEL (Rlt (add_SNo yi (minus_SNo eps)) zi) (Rlt zi (add_SNo yi eps)) HziConj).
We prove the intermediate claim HrightR: Rlt zi (add_SNo yi eps).
An exact proof term for the current goal is (andER (Rlt (add_SNo yi (minus_SNo eps)) zi) (Rlt zi (add_SNo yi eps)) HziConj).
We prove the intermediate claim HyimepsR: add_SNo yi (minus_SNo eps) ∈ R.
An exact proof term for the current goal is (real_add_SNo yi HyiR (minus_SNo eps) (real_minus_SNo eps HepsR)).
We prove the intermediate claim HyiepsR: add_SNo yi eps ∈ R.
An exact proof term for the current goal is (real_add_SNo yi HyiR eps HepsR).
We prove the intermediate claim HyimepsS: SNo (add_SNo yi (minus_SNo eps)).
An exact proof term for the current goal is (real_SNo (add_SNo yi (minus_SNo eps)) HyimepsR).
We prove the intermediate claim HyiepsS: SNo (add_SNo yi eps).
An exact proof term for the current goal is (real_SNo (add_SNo yi eps) HyiepsR).
We prove the intermediate claim HleftS: add_SNo yi (minus_SNo eps) < zi.
An exact proof term for the current goal is (RltE_lt (add_SNo yi (minus_SNo eps)) zi HleftR).
We prove the intermediate claim HrightS: zi < add_SNo yi eps.
An exact proof term for the current goal is (RltE_lt zi (add_SNo yi eps) HrightR).
Set t to be the term add_SNo yi (minus_SNo zi).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (real_add_SNo yi HyiR (minus_SNo zi) (real_minus_SNo zi HziR)).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmYiS: SNo (minus_SNo yi).
An exact proof term for the current goal is (SNo_minus_SNo yi HyiS).
We prove the intermediate claim HmZiS: SNo (minus_SNo zi).
An exact proof term for the current goal is (SNo_minus_SNo zi HziS).
We prove the intermediate claim HmepsS: SNo (minus_SNo eps).
An exact proof term for the current goal is (SNo_minus_SNo eps HepsS).
We prove the intermediate claim HdiffLt1: add_SNo (minus_SNo yi) zi < add_SNo (minus_SNo yi) (add_SNo yi eps).
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo yi) zi (add_SNo yi eps) HmYiS HziS HyiepsS HrightS).
We prove the intermediate claim HdiffLt2: add_SNo zi (minus_SNo yi) < eps.
We will prove add_SNo zi (minus_SNo yi) < eps.
rewrite the current goal using (add_SNo_com (minus_SNo yi) zi HmYiS HziS) (from right to left) at position 1.
We prove the intermediate claim HRhs: add_SNo (minus_SNo yi) (add_SNo yi eps) = eps.
We prove the intermediate claim Hassoc: add_SNo (minus_SNo yi) (add_SNo yi eps) = add_SNo (add_SNo (minus_SNo yi) yi) eps.
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo yi) yi eps HmYiS HyiS HepsS).
rewrite the current goal using Hassoc (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_linv yi HyiS) (from left to right).
rewrite the current goal using (add_SNo_0L eps HepsS) (from left to right).
Use reflexivity.
rewrite the current goal using HRhs (from right to left).
An exact proof term for the current goal is HdiffLt1.
We prove the intermediate claim HmDiff: minus_SNo eps < minus_SNo (add_SNo zi (minus_SNo yi)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (add_SNo zi (minus_SNo yi)) eps (SNo_add_SNo zi (minus_SNo yi) HziS HmYiS) HepsS HdiffLt2).
We prove the intermediate claim HmDiffEq: minus_SNo (add_SNo zi (minus_SNo yi)) = t.
rewrite the current goal using (minus_add_SNo_distr zi (minus_SNo yi) HziS HmYiS) (from left to right).
rewrite the current goal using (minus_SNo_invol yi HyiS) (from left to right).
rewrite the current goal using (add_SNo_com (minus_SNo zi) yi HmZiS HyiS) (from left to right).
Use reflexivity.
We prove the intermediate claim HloLt: minus_SNo eps < t.
rewrite the current goal using HmDiffEq (from right to left).
An exact proof term for the current goal is HmDiff.
We prove the intermediate claim HdiffLt3: add_SNo (minus_SNo yi) (add_SNo yi (minus_SNo eps)) < add_SNo (minus_SNo yi) zi.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo yi) (add_SNo yi (minus_SNo eps)) zi HmYiS HyimepsS HziS HleftS).
We prove the intermediate claim HdiffLt4: minus_SNo eps < add_SNo zi (minus_SNo yi).
We will prove minus_SNo eps < add_SNo zi (minus_SNo yi).
rewrite the current goal using (add_SNo_com (minus_SNo yi) zi HmYiS HziS) (from right to left).
We prove the intermediate claim HLhs: add_SNo (minus_SNo yi) (add_SNo yi (minus_SNo eps)) = minus_SNo eps.
We prove the intermediate claim Hassoc2: add_SNo (minus_SNo yi) (add_SNo yi (minus_SNo eps)) = add_SNo (add_SNo (minus_SNo yi) yi) (minus_SNo eps).
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo yi) yi (minus_SNo eps) HmYiS HyiS HmepsS).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_linv yi HyiS) (from left to right).
rewrite the current goal using (add_SNo_0L (minus_SNo eps) HmepsS) (from left to right).
Use reflexivity.
rewrite the current goal using HLhs (from right to left) at position 1.
An exact proof term for the current goal is HdiffLt3.
We prove the intermediate claim HtLt: t < eps.
rewrite the current goal using HmDiffEq (from right to left).
rewrite the current goal using (minus_SNo_invol eps HepsS) (from right to left).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo eps) (add_SNo zi (minus_SNo yi)) HmepsS (SNo_add_SNo zi (minus_SNo yi) HziS HmYiS) HdiffLt4).
We prove the intermediate claim Hlo: minus_SNo eps ≤ t.
An exact proof term for the current goal is (SNoLtLe (minus_SNo eps) t HloLt).
We prove the intermediate claim Hhi: t ≤ eps.
An exact proof term for the current goal is (SNoLtLe t eps HtLt).
We prove the intermediate claim HabsLe: abs_SNo t ≤ eps.
An exact proof term for the current goal is (abs_SNo_Le_of_bounds t eps HtS HepsS Hlo Hhi).
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HabsS: SNo (abs_SNo t).
An exact proof term for the current goal is (SNo_abs_SNo t HtS).
We prove the intermediate claim HepsLt1S: eps < 1.
An exact proof term for the current goal is (RltE_lt eps 1 HepsLt1).
We prove the intermediate claim HabsLt1S: abs_SNo t < 1.
An exact proof term for the current goal is (SNoLeLt_tra (abs_SNo t) eps 1 HabsS HepsS SNo_1 HabsLe HepsLt1S).
We prove the intermediate claim HabsLt1R: Rlt (abs_SNo t) 1.
An exact proof term for the current goal is (RltI (abs_SNo t) 1 HabsR real_1 HabsLt1S).
We prove the intermediate claim HbdEq: bd = abs_SNo t.
We prove the intermediate claim HbdDef: bd = If_i (Rlt (abs_SNo (add_SNo yi (minus_SNo zi))) 1) (abs_SNo (add_SNo yi (minus_SNo zi))) 1.
Use reflexivity.
rewrite the current goal using HbdDef (from left to right).
rewrite the current goal using (If_i_1 (Rlt (abs_SNo (add_SNo yi (minus_SNo zi))) 1) (abs_SNo (add_SNo yi (minus_SNo zi))) 1 HabsLt1R) (from left to right).
Use reflexivity.
We prove the intermediate claim HbdLe: bd ≤ eps.
rewrite the current goal using HbdEq (from left to right).
An exact proof term for the current goal is HabsLe.
We prove the intermediate claim HsuccNotIn0: ordsucc i0 ∉ {0}.
Assume Hin0: ordsucc i0 ∈ {0}.
We prove the intermediate claim Heq0: ordsucc i0 = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc i0) Hin0).
An exact proof term for the current goal is (neq_ordsucc_0 i0 Heq0).
We prove the intermediate claim HiIn: ordsucc i0 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc i0) HSi0 HsuccNotIn0).
We prove the intermediate claim HinvRle1: Rle inv 1.
An exact proof term for the current goal is (inv_nat_Rle_1 (ordsucc i0) HiIn).
We prove the intermediate claim HinvLe1: inv ≤ 1.
Apply (SNoLt_trichotomy_or_impred inv 1 HinvS SNo_1 (inv ≤ 1)) to the current goal.
Assume Hlt: inv < 1.
An exact proof term for the current goal is (SNoLtLe inv 1 Hlt).
Assume Heq: inv = 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref 1).
Assume H1lt: 1 < inv.
Apply FalseE to the current goal.
We prove the intermediate claim HinvRlt: Rlt 1 inv.
An exact proof term for the current goal is (RltI 1 inv real_1 HinvR H1lt).
An exact proof term for the current goal is ((RleE_nlt inv 1 HinvRle1) HinvRlt).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos (ordsucc i0) HiIn).
We prove the intermediate claim HinvPosS: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPosR).
We prove the intermediate claim HinvNN: 0 ≤ inv.
An exact proof term for the current goal is (SNoLtLe 0 inv HinvPosS).
We prove the intermediate claim HbdNN: 0 ≤ bd.
An exact proof term for the current goal is (R_bounded_distance_nonneg yi zi HyiR HziR).
We prove the intermediate claim HmulLe: mul_SNo bd inv ≤ eps.
We prove the intermediate claim HmulLe': mul_SNo bd inv ≤ mul_SNo eps 1.
An exact proof term for the current goal is (nonneg_mul_SNo_Le2 bd inv eps 1 HbdS HinvS HepsS SNo_1 HbdNN HinvNN HbdLe HinvLe1).
We will prove mul_SNo bd inv ≤ eps.
rewrite the current goal using (mul_SNo_oneR eps HepsS) (from right to left).
An exact proof term for the current goal is HmulLe'.
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo bd inv) eps HmulR HepsR HmulLe).
Assume Hnot: ¬ (i0 ∈ I).
Set yi to be the term apply_fun y i0.
Set zi to be the term apply_fun z i0.
Set bd to be the term R_bounded_distance yi zi.
Set inv to be the term inv_nat (ordsucc i0).
We prove the intermediate claim HyiR: yi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R y i0 HyX Hi0O).
We prove the intermediate claim HziR: zi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R z i0 HzX Hi0O).
We prove the intermediate claim HyiS: SNo yi.
An exact proof term for the current goal is (real_SNo yi HyiR).
We prove the intermediate claim HziS: SNo zi.
An exact proof term for the current goal is (real_SNo zi HziR).
We prove the intermediate claim HbdR: bd ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R yi zi HyiR HziR).
We prove the intermediate claim HbdS: SNo bd.
An exact proof term for the current goal is (real_SNo bd HbdR).
We prove the intermediate claim HSi0: ordsucc i0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i0 Hi0O).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i0) HSi0).
We prove the intermediate claim HinvS: SNo inv.
An exact proof term for the current goal is (real_SNo inv HinvR).
We prove the intermediate claim HmulR: mul_SNo bd inv ∈ R.
An exact proof term for the current goal is (real_mul_SNo bd HbdR inv HinvR).
We prove the intermediate claim Hi0Ord: ordinal i0.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i0 Hi0O).
We prove the intermediate claim HIdef0: I = ordsucc N.
Use reflexivity.
We prove the intermediate claim HNOrd: ordinal N.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N HNO).
We prove the intermediate claim HIOrd: ordinal I.
rewrite the current goal using HIdef0 (from left to right).
An exact proof term for the current goal is (ordinal_ordsucc N HNOrd).
We prove the intermediate claim Hcases: i0 ∈ I ∨ I ⊆ i0.
An exact proof term for the current goal is (ordinal_In_Or_Subq i0 I Hi0Ord HIOrd).
We prove the intermediate claim HIc: I ⊆ i0.
Apply (Hcases (I ⊆ i0)) to the current goal.
Assume Hi0InI: i0 ∈ I.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnot Hi0InI).
Assume Hsub: I ⊆ i0.
An exact proof term for the current goal is Hsub.
We prove the intermediate claim HNInI: N ∈ I.
rewrite the current goal using HIdef0 (from left to right).
An exact proof term for the current goal is (ordsuccI2 N).
We prove the intermediate claim HNi0: N ∈ i0.
An exact proof term for the current goal is (HIc N HNInI).
We prove the intermediate claim HinvLtN: Rlt (inv_nat (ordsucc i0)) (inv_nat (ordsucc N)).
An exact proof term for the current goal is (inv_nat_ordsucc_antitone N i0 HNO Hi0O HNi0).
We prove the intermediate claim HinvLt: Rlt (inv_nat (ordsucc i0)) eps.
An exact proof term for the current goal is (Rlt_tra (inv_nat (ordsucc i0)) (inv_nat (ordsucc N)) eps HinvLtN HinvNLt).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HinvLtS: inv < eps.
An exact proof term for the current goal is (RltE_lt inv eps HinvLt).
We prove the intermediate claim HinvLe: inv ≤ eps.
An exact proof term for the current goal is (SNoLtLe inv eps HinvLtS).
We prove the intermediate claim HbdLe1R: Rle bd 1.
An exact proof term for the current goal is (R_bounded_distance_le_1 yi zi HyiR HziR).
We prove the intermediate claim HbdLe1: bd ≤ 1.
Apply (SNoLt_trichotomy_or_impred bd 1 HbdS SNo_1 (bd ≤ 1)) to the current goal.
Assume Hlt: bd < 1.
An exact proof term for the current goal is (SNoLtLe bd 1 Hlt).
Assume Heq: bd = 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref 1).
Assume H1lt: 1 < bd.
Apply FalseE to the current goal.
We prove the intermediate claim HbdRlt: Rlt 1 bd.
An exact proof term for the current goal is (RltI 1 bd real_1 HbdR H1lt).
An exact proof term for the current goal is ((RleE_nlt bd 1 HbdLe1R) HbdRlt).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
Set mi to be the term ordsucc i0.
We prove the intermediate claim HmiNotIn0: mi ∉ {0}.
Assume Hin0: mi ∈ {0}.
We prove the intermediate claim Heq0: mi = 0.
An exact proof term for the current goal is (SingE 0 mi Hin0).
An exact proof term for the current goal is (neq_ordsucc_0 i0 Heq0).
We prove the intermediate claim HmiIn: mi ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} mi HSi0 HmiNotIn0).
An exact proof term for the current goal is (inv_nat_pos mi HmiIn).
We prove the intermediate claim HinvPosS: 0 < inv.
An exact proof term for the current goal is (RltE_lt 0 inv HinvPosR).
We prove the intermediate claim HinvNN: 0 ≤ inv.
An exact proof term for the current goal is (SNoLtLe 0 inv HinvPosS).
We prove the intermediate claim HmulLeInv: mul_SNo bd inv ≤ inv.
An exact proof term for the current goal is (mul_SNo_Le1_nonneg_Le bd inv HbdS HinvS HbdLe1 HinvNN).
We prove the intermediate claim HmulS: SNo (mul_SNo bd inv).
An exact proof term for the current goal is (real_SNo (mul_SNo bd inv) HmulR).
We prove the intermediate claim HmulLe: mul_SNo bd inv ≤ eps.
An exact proof term for the current goal is (SNoLe_tra (mul_SNo bd inv) inv eps HmulS HinvS HepsS HmulLeInv HinvLe).
An exact proof term for the current goal is (Rle_of_SNoLe (mul_SNo bd inv) eps HmulR HepsR HmulLe).
We prove the intermediate claim Hle': Rle l eps.
An exact proof term for the current goal is (HlubMin eps HepsR Hub).
An exact proof term for the current goal is Hle'.
We prove the intermediate claim HsumLe: Rle (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) (add_SNo (apply_fun d (x,y)) eps).
An exact proof term for the current goal is (Rle_add_SNo_2 (apply_fun d (x,y)) (apply_fun d (y,z)) eps HdxyR HdyzR HepsR HdyzLe).
We prove the intermediate claim HgapLt: Rlt eps gap.
An exact proof term for the current goal is HepsLtGap.
We prove the intermediate claim HsumLt': Rlt (add_SNo (apply_fun d (x,y)) eps) r.
We prove the intermediate claim HdxyS: SNo (apply_fun d (x,y)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,y)) HdxyR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
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 HgapR: gap ∈ R.
An exact proof term for the current goal is (RltE_right eps gap HgapLt).
We prove the intermediate claim HgapS: SNo gap.
An exact proof term for the current goal is (real_SNo gap HgapR).
We prove the intermediate claim HepsltgapS: eps < gap.
An exact proof term for the current goal is (RltE_lt eps gap HgapLt).
We prove the intermediate claim HsumLtS: add_SNo (apply_fun d (x,y)) eps < add_SNo (apply_fun d (x,y)) gap.
An exact proof term for the current goal is (add_SNo_Lt2 (apply_fun d (x,y)) eps gap HdxyS HepsS HgapS HepsltgapS).
We prove the intermediate claim HgapDef: gap = add_SNo r (minus_SNo (apply_fun d (x,y))).
Use reflexivity.
We prove the intermediate claim HsumEq: add_SNo (apply_fun d (x,y)) gap = r.
rewrite the current goal using HgapDef (from left to right).
We prove the intermediate claim HmdxyS: SNo (minus_SNo (apply_fun d (x,y))).
An exact proof term for the current goal is (SNo_minus_SNo (apply_fun d (x,y)) HdxyS).
rewrite the current goal using (add_SNo_assoc (apply_fun d (x,y)) r (minus_SNo (apply_fun d (x,y))) HdxyS HrS HmdxyS) (from left to right).
We prove the intermediate claim Hcom: add_SNo (apply_fun d (x,y)) r = add_SNo r (apply_fun d (x,y)).
An exact proof term for the current goal is (add_SNo_com (apply_fun d (x,y)) r HdxyS HrS).
rewrite the current goal using Hcom (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc r (apply_fun d (x,y)) (minus_SNo (apply_fun d (x,y))) HrS HdxyS HmdxyS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv (apply_fun d (x,y)) HdxyS) (from left to right).
rewrite the current goal using (add_SNo_0R r HrS) (from left to right).
Use reflexivity.
We prove the intermediate claim HsumLtS2: add_SNo (apply_fun d (x,y)) eps < r.
rewrite the current goal using HsumEq (from right to left).
An exact proof term for the current goal is HsumLtS.
We prove the intermediate claim HsumR: add_SNo (apply_fun d (x,y)) eps ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (x,y)) HdxyR eps HepsR).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x,y)) eps) r HsumR HrR HsumLtS2).
We prove the intermediate claim HsumLt: Rlt (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) r.
An exact proof term for the current goal is (Rle_Rlt_tra (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) (add_SNo (apply_fun d (x,y)) eps) r HsumLe HsumLt').
We prove the intermediate claim HdxzLt: Rlt (apply_fun d (x,z)) r.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (x,z)) (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) r Htri HsumLt).
An exact proof term for the current goal is (open_ballI X d x r z HzX HdxzLt).
Apply HexF to the current goal.
Let F be given.
Assume HFcore.
We prove the intermediate claim HFleft: F ∈ finite_subcollections S ∧ y ∈ intersection_of_family X F.
Apply HFcore to the current goal.
Assume HFleft HFsub.
An exact proof term for the current goal is HFleft.
We prove the intermediate claim HFsub: intersection_of_family X F ⊆ open_ball X d x r.
Apply HFcore to the current goal.
Assume HFleft HFsub.
An exact proof term for the current goal is HFsub.
We prove the intermediate claim HF: F ∈ finite_subcollections S.
Apply HFleft to the current goal.
Assume HF HyIn.
An exact proof term for the current goal is HF.
We prove the intermediate claim HyIn: y ∈ intersection_of_family X F.
Apply HFleft to the current goal.
Assume HF HyIn.
An exact proof term for the current goal is HyIn.
We use (intersection_of_family X F) to witness the existential quantifier.
Apply andI to the current goal.
We will prove intersection_of_family X F ∈ B.
We prove the intermediate claim Hnon: intersection_of_family X F ≠ Empty.
Assume Heq: intersection_of_family X F = Empty.
We will prove False.
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyIn.
An exact proof term for the current goal is (EmptyE y HyE).
An exact proof term for the current goal is (finite_intersection_in_basis X S F HF Hnon).
Apply andI to the current goal.
An exact proof term for the current goal is HyIn.
An exact proof term for the current goal is HFsub.
∎