Let i and U be given.
Assume Hm: metric_on R_omega_space Romega_D_metric.
Assume Hi: i ∈ ω.
Assume HU: U ∈ R_standard_topology.
Set Xi0 to be the term const_space_family ω R R_standard_topology.
Set C to be the term product_cylinder ω Xi0 i U.
Set X to be the term R_omega_space.
Set d to be the term Romega_D_metric.
We prove the intermediate claim HXeq: X = product_space ω Xi0.
Use reflexivity.
Set Tm to be the term metric_topology X d.
Set B to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HTm: topology_on X Tm.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We will prove C ∈ Tm.
We prove the intermediate claim HTdef: Tm = generated_topology X B.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We will prove C ∈ generated_topology X B.
We prove the intermediate claim Hgendef: generated_topology X B = {U0 ∈ 𝒫 X|∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0}.
Use reflexivity.
rewrite the current goal using Hgendef (from left to right).
Apply SepI to the current goal.
We will prove C ∈ 𝒫 X.
Apply PowerI to the current goal.
Let f be given.
Assume HfC: f ∈ C.
We will prove f ∈ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (SepE1 (product_space ω Xi0) (λg0 : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi0 i ∧ apply_fun g0 i ∈ U) f HfC).
Let f be given.
Assume HfC: f ∈ C.
We will prove ∃b ∈ B, f ∈ b ∧ b ⊆ C.
We prove the intermediate claim HfX: f ∈ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (SepE1 (product_space ω Xi0) (λg0 : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi0 i ∧ apply_fun g0 i ∈ U) f HfC).
We prove the intermediate claim Hfprop: i ∈ ω ∧ U ∈ space_family_topology Xi0 i ∧ apply_fun f i ∈ U.
An exact proof term for the current goal is (SepE2 (product_space ω Xi0) (λg0 : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi0 i ∧ apply_fun g0 i ∈ U) f HfC).
We prove the intermediate claim Hcore: i ∈ ω ∧ U ∈ space_family_topology Xi0 i.
An exact proof term for the current goal is (andEL (i ∈ ω ∧ U ∈ space_family_topology Xi0 i) (apply_fun f i ∈ U) Hfprop).
We prove the intermediate claim HfiU: apply_fun f i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi0 i) (apply_fun f i ∈ U) Hfprop).
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HUneigh: ∀x0 ∈ U, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim Hexb0: ∃b0 ∈ R_standard_basis, apply_fun f i ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUneigh (apply_fun f i) HfiU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
Apply Hb0pair to the current goal.
Assume Hb0Std: b0 ∈ R_standard_basis.
Assume Hb0prop: apply_fun f i ∈ b0 ∧ b0 ⊆ U.
We prove the intermediate claim Hxib0: apply_fun f i ∈ b0.
An exact proof term for the current goal is (andEL (apply_fun f i ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (apply_fun f i ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hexa: ∃a ∈ R, b0 ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) b0 Hb0Std).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
Apply Hapair to the current goal.
Assume HaR: a ∈ R.
Assume Hb0fam: b0 ∈ {open_interval a b|b ∈ R}.
We prove the intermediate claim Hexb: ∃b ∈ R, b0 = open_interval a b.
An exact proof term for the current goal is (ReplE R (λb1 : set ⇒ open_interval a b1) b0 Hb0fam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbR: b ∈ R.
Assume Hb0eq: b0 = open_interval a b.
We prove the intermediate claim Hxib0': apply_fun f i ∈ open_interval a b.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxib0.
We prove the intermediate claim Hxiprop: Rlt a (apply_fun f i) ∧ Rlt (apply_fun f i) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) (apply_fun f i) Hxib0').
We prove the intermediate claim Hailt: Rlt a (apply_fun f i).
An exact proof term for the current goal is (andEL (Rlt a (apply_fun f i)) (Rlt (apply_fun f i) b) Hxiprop).
We prove the intermediate claim Hiltb: Rlt (apply_fun f i) b.
An exact proof term for the current goal is (andER (Rlt a (apply_fun f i)) (Rlt (apply_fun f i) b) Hxiprop).
We prove the intermediate claim HexBall: ∃r0 : set, r0 ∈ R ∧ Rlt 0 r0 ∧ open_ball X d f r0 ⊆ C.
Set xi to be the term apply_fun f i.
We prove the intermediate claim HxiR: xi ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R f i HfX Hi).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HxiS: SNo xi.
An exact proof term for the current goal is (real_SNo xi HxiR).
Set m1 to be the term add_SNo xi (minus_SNo a).
Set m2 to be the term add_SNo b (minus_SNo xi).
We prove the intermediate claim Hm1R: m1 ∈ R.
An exact proof term for the current goal is (real_add_SNo xi HxiR (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim Hm2R: m2 ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo xi) (real_minus_SNo xi HxiR)).
We prove the intermediate claim Hm1pos: Rlt 0 m1.
We prove the intermediate claim Haxlt: a < xi.
An exact proof term for the current goal is (RltE_lt a xi Hailt).
We prove the intermediate claim Hm1posS: 0 < m1.
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim Hlt: add_SNo (minus_SNo a) a < add_SNo (minus_SNo a) xi.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo a) a xi HmaS HaS HxiS Haxlt).
We prove the intermediate claim H0eq: add_SNo (minus_SNo a) a = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv a HaS).
We prove the intermediate claim Hm1eq: add_SNo (minus_SNo a) xi = m1.
We prove the intermediate claim Hcom: add_SNo (minus_SNo a) xi = add_SNo xi (minus_SNo a).
An exact proof term for the current goal is (add_SNo_com (minus_SNo a) xi HmaS HxiS).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hm1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (RltI 0 m1 real_0 Hm1R Hm1posS).
We prove the intermediate claim Hm2pos: Rlt 0 m2.
We prove the intermediate claim Hxblt: xi < b.
An exact proof term for the current goal is (RltE_lt xi b Hiltb).
We prove the intermediate claim Hm2posS: 0 < m2.
We prove the intermediate claim HmxiS: SNo (minus_SNo xi).
An exact proof term for the current goal is (SNo_minus_SNo xi HxiS).
We prove the intermediate claim Hlt: add_SNo (minus_SNo xi) xi < add_SNo (minus_SNo xi) b.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo xi) xi b HmxiS HxiS HbS Hxblt).
We prove the intermediate claim H0eq: add_SNo (minus_SNo xi) xi = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv xi HxiS).
We prove the intermediate claim Hm2eq: add_SNo (minus_SNo xi) b = m2.
We prove the intermediate claim Hcom: add_SNo (minus_SNo xi) b = add_SNo b (minus_SNo xi).
An exact proof term for the current goal is (add_SNo_com (minus_SNo xi) b HmxiS HbS).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hm2eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (RltI 0 m2 real_0 Hm2R Hm2posS).
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 Hexr3: ∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 m1 ∧ Rlt r3 m2 ∧ Rlt r3 1 ∧ Rlt r3 1.
An exact proof term for the current goal is (exists_eps_lt_four_pos_Euclid m1 m2 1 1 Hm1R Hm2R H1R H1R Hm1pos Hm2pos H1pos H1pos).
Apply Hexr3 to the current goal.
Let r3 be given.
Assume Hr3conj: r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 m1 ∧ Rlt r3 m2 ∧ Rlt r3 1 ∧ Rlt r3 1.
We prove the intermediate claim Hr3top: ((((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) ∧ Rlt r3 1) ∧ Rlt r3 1.
An exact proof term for the current goal is Hr3conj.
We prove the intermediate claim Hr3top1: (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) ∧ Rlt r3 1.
Apply Hr3top to the current goal.
Assume Hr3top1 Hr3lt1b.
An exact proof term for the current goal is Hr3top1.
We prove the intermediate claim Hr3top2: ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2.
Apply Hr3top1 to the current goal.
Assume Hr3top2 Hr3lt1.
An exact proof term for the current goal is Hr3top2.
We prove the intermediate claim Hr3top3: (r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1.
Apply Hr3top2 to the current goal.
Assume Hr3top3 Hr3m2.
An exact proof term for the current goal is Hr3top3.
We prove the intermediate claim Hr3pair: r3 ∈ R ∧ Rlt 0 r3.
Apply Hr3top3 to the current goal.
Assume Hr3pair Hr3m1.
An exact proof term for the current goal is Hr3pair.
We prove the intermediate claim Hr3R: r3 ∈ R.
Apply Hr3pair to the current goal.
Assume Hr3R Hr3pos.
An exact proof term for the current goal is Hr3R.
We prove the intermediate claim Hr3pos: Rlt 0 r3.
Apply Hr3pair to the current goal.
Assume Hr3R Hr3pos.
An exact proof term for the current goal is Hr3pos.
We prove the intermediate claim Hr3lt1b: Rlt r3 1.
Apply Hr3top to the current goal.
Assume Hr3top1 Hr3lt1b.
An exact proof term for the current goal is Hr3lt1b.
We prove the intermediate claim Hr3lt1: Rlt r3 1.
Apply Hr3top1 to the current goal.
Assume Hr3top2 Hr3lt1.
An exact proof term for the current goal is Hr3lt1.
We prove the intermediate claim Hr3m2lt: Rlt r3 m2.
Apply Hr3top2 to the current goal.
Assume Hr3top3 Hr3m2lt.
An exact proof term for the current goal is Hr3m2lt.
We prove the intermediate claim Hr3m1lt: Rlt r3 m1.
Apply Hr3top3 to the current goal.
Assume Hr3pair Hr3m1lt.
An exact proof term for the current goal is Hr3m1lt.
Set inv to be the term inv_nat (ordsucc i).
We prove the intermediate claim Hisuc: ordsucc i ∈ ω.
An exact proof term for the current goal is (omega_ordsucc i Hi).
We prove the intermediate claim HsuccNotIn0: ordsucc i ∉ {0}.
Assume Hin0: ordsucc i ∈ {0}.
We prove the intermediate claim Heq: ordsucc i = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc i) Hin0).
An exact proof term for the current goal is (neq_ordsucc_0 i Heq).
We prove the intermediate claim HiIn: ordsucc i ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc i) Hisuc HsuccNotIn0).
We prove the intermediate claim HinvR: inv ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc i) Hisuc).
We prove the intermediate claim HinvPosR: Rlt 0 inv.
An exact proof term for the current goal is (inv_nat_pos (ordsucc i) HiIn).
Set r0 to be the term mul_SNo r3 inv.
We prove the intermediate claim Hr0R: r0 ∈ R.
An exact proof term for the current goal is (real_mul_SNo r3 Hr3R inv HinvR).
We prove the intermediate claim Hr0pos: Rlt 0 r0.
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (real_SNo r3 Hr3R).
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 Hr3posS: 0 < r3.
An exact proof term for the current goal is (RltE_lt 0 r3 Hr3pos).
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 Hr0posS: 0 < r0.
An exact proof term for the current goal is (mul_SNo_pos_pos r3 inv Hr3S HinvS Hr3posS HinvPosS).
An exact proof term for the current goal is (RltI 0 r0 real_0 Hr0R Hr0posS).
We use r0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hr0R.
An exact proof term for the current goal is Hr0pos.
Let g be given.
Assume Hgball: g ∈ open_ball X d f r0.
We will prove g ∈ C.
We prove the intermediate claim HgX: g ∈ X.
An exact proof term for the current goal is (open_ballE1 X d f r0 g Hgball).
We prove the intermediate claim Hgprod: g ∈ product_space ω Xi0.
rewrite the current goal using HXeq (from right to left).
An exact proof term for the current goal is HgX.
We prove the intermediate claim HCdef: C = {f0 ∈ product_space ω Xi0|(i ∈ ω ∧ U ∈ space_family_topology Xi0 i) ∧ apply_fun f0 i ∈ U}.
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 Hgprod.
We will prove (i ∈ ω ∧ U ∈ space_family_topology Xi0 i) ∧ apply_fun g i ∈ U.
We prove the intermediate claim Hleft: i ∈ ω ∧ U ∈ space_family_topology Xi0 i.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate claim HTi: space_family_topology Xi0 i = R_standard_topology.
We prove the intermediate claim Hdef: space_family_topology Xi0 i = (apply_fun Xi0 i) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (const_space_family_apply ω R R_standard_topology i Hi) (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
rewrite the current goal using HTi (from left to right).
An exact proof term for the current goal is HU.
Apply (andI (i ∈ ω ∧ U ∈ space_family_topology Xi0 i) (apply_fun g i ∈ U)) to the current goal.
An exact proof term for the current goal is Hleft.
We prove the intermediate claim HgiR: apply_fun g i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R g i HgX Hi).
We prove the intermediate claim Hfgprod: (f,g) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X f g HfX HgX).
We prove the intermediate claim Hdapp: apply_fun d (f,g) = Romega_D_metric_value f g.
rewrite the current goal using (apply_fun_graph (setprod X X) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (f,g) Hfgprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq f g) (from left to right).
rewrite the current goal using (tuple_2_1_eq f g) (from left to right).
Use reflexivity.
We prove the intermediate claim Hltball: Rlt (apply_fun d (f,g)) r0.
An exact proof term for the current goal is (open_ballE2 X d f r0 g Hgball).
We prove the intermediate claim Hltval: Rlt (Romega_D_metric_value f g) r0.
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 Habfg: abs_SNo (add_SNo xi (minus_SNo (apply_fun g i))) < r3.
We prove the intermediate claim Hr0eq: r0 = mul_SNo r3 (inv_nat (ordsucc i)).
Use reflexivity.
We prove the intermediate claim Hltval2: Rlt (Romega_D_metric_value f g) (mul_SNo r3 (inv_nat (ordsucc i))).
rewrite the current goal using Hr0eq (from right to left).
An exact proof term for the current goal is Hltval.
An exact proof term for the current goal is (Romega_D_metric_coord_abs_lt f g i r3 HfX HgX Hi Hr3R Hr3pos Hr3lt1 Hltval2).
We prove the intermediate claim Hgib: apply_fun g i ∈ open_interval a b.
Set t to be the term add_SNo xi (minus_SNo (apply_fun g i)).
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (real_SNo r3 Hr3R).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (RltE_lt 0 r3 Hr3pos).
We prove the intermediate claim Hm1S: SNo m1.
An exact proof term for the current goal is (real_SNo m1 Hm1R).
We prove the intermediate claim Hm2S: SNo m2.
An exact proof term for the current goal is (real_SNo m2 Hm2R).
We prove the intermediate claim Hr3m1ltS: r3 < m1.
An exact proof term for the current goal is (RltE_lt r3 m1 Hr3m1lt).
We prove the intermediate claim Hr3m2ltS: r3 < m2.
An exact proof term for the current goal is (RltE_lt r3 m2 Hr3m2lt).
We prove the intermediate claim HgiS: SNo (apply_fun g i).
An exact proof term for the current goal is (real_SNo (apply_fun g i) HgiR).
We prove the intermediate claim HmtS: SNo (minus_SNo (apply_fun g i)).
An exact proof term for the current goal is (SNo_minus_SNo (apply_fun g i) HgiS).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (SNo_add_SNo xi (minus_SNo (apply_fun g i)) HxiS HmtS).
We prove the intermediate claim Htlt: t < r3.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt t r3 HtS Hr3S Hr3posS Habfg).
We prove the intermediate claim Hmtlt: minus_SNo t < r3.
An exact proof term for the current goal is (abs_SNo_lt_imp_neg_lt t r3 HtS Hr3S Hr3posS Habfg).
We prove the intermediate claim HinterDef: open_interval a b = {x0 ∈ R|Rlt a x0 ∧ Rlt x0 b}.
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 HgiR.
We will prove Rlt a (apply_fun g i) ∧ Rlt (apply_fun g i) b.
Apply andI to the current goal.
We will prove Rlt a (apply_fun g i).
We prove the intermediate claim Htltm1: t < m1.
An exact proof term for the current goal is (SNoLt_tra t r3 m1 HtS Hr3S Hm1S Htlt Hr3m1ltS).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim Htdef: t = add_SNo xi (minus_SNo (apply_fun g i)).
Use reflexivity.
We prove the intermediate claim Hm1def: m1 = add_SNo xi (minus_SNo a).
Use reflexivity.
We prove the intermediate claim Htltm1': add_SNo xi (minus_SNo (apply_fun g i)) < add_SNo xi (minus_SNo a).
rewrite the current goal using Htdef (from right to left).
rewrite the current goal using Hm1def (from right to left).
An exact proof term for the current goal is Htltm1.
We prove the intermediate claim Hneglt: minus_SNo (apply_fun g i) < minus_SNo a.
An exact proof term for the current goal is (add_SNo_Lt2_cancel xi (minus_SNo (apply_fun g i)) (minus_SNo a) HxiS HmtS HmaS Htltm1').
We prove the intermediate claim Hnegneg: minus_SNo (minus_SNo a) < minus_SNo (minus_SNo (apply_fun g i)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo (apply_fun g i)) (minus_SNo a) HmtS HmaS Hneglt).
We prove the intermediate claim Hainv: minus_SNo (minus_SNo a) = a.
An exact proof term for the current goal is (minus_SNo_invol a HaS).
We prove the intermediate claim Hgiinv: minus_SNo (minus_SNo (apply_fun g i)) = apply_fun g i.
An exact proof term for the current goal is (minus_SNo_invol (apply_fun g i) HgiS).
We prove the intermediate claim HaltS: a < apply_fun g i.
rewrite the current goal using Hainv (from right to left) at position 1.
rewrite the current goal using Hgiinv (from right to left).
An exact proof term for the current goal is Hnegneg.
An exact proof term for the current goal is (RltI a (apply_fun g i) HaR HgiR HaltS).
We will prove Rlt (apply_fun g i) b.
We prove the intermediate claim Hmtltm2: minus_SNo t < m2.
An exact proof term for the current goal is (SNoLt_tra (minus_SNo t) r3 m2 (SNo_minus_SNo t HtS) Hr3S Hm2S Hmtlt Hr3m2ltS).
We prove the intermediate claim HmxiS: SNo (minus_SNo xi).
An exact proof term for the current goal is (SNo_minus_SNo xi HxiS).
We prove the intermediate claim Hm2def: m2 = add_SNo b (minus_SNo xi).
Use reflexivity.
We prove the intermediate claim Hnegtdistr: minus_SNo t = add_SNo (minus_SNo xi) (minus_SNo (minus_SNo (apply_fun g i))).
An exact proof term for the current goal is (minus_add_SNo_distr xi (minus_SNo (apply_fun g i)) HxiS HmtS).
We prove the intermediate claim Hgiinv2: minus_SNo (minus_SNo (apply_fun g i)) = apply_fun g i.
An exact proof term for the current goal is (minus_SNo_invol (apply_fun g i) HgiS).
We prove the intermediate claim Hnegteq: minus_SNo t = add_SNo (minus_SNo xi) (apply_fun g i).
rewrite the current goal using Hgiinv2 (from right to left) at position 2.
An exact proof term for the current goal is Hnegtdistr.
We prove the intermediate claim Hnegteq2: add_SNo (apply_fun g i) (minus_SNo xi) = minus_SNo t.
We prove the intermediate claim Hcom: add_SNo (minus_SNo xi) (apply_fun g i) = add_SNo (apply_fun g i) (minus_SNo xi).
An exact proof term for the current goal is (add_SNo_com (minus_SNo xi) (apply_fun g i) HmxiS HgiS).
rewrite the current goal using Hcom (from right to left).
rewrite the current goal using Hnegteq (from right to left).
Use reflexivity.
We prove the intermediate claim Hineq: add_SNo (apply_fun g i) (minus_SNo xi) < add_SNo b (minus_SNo xi).
rewrite the current goal using Hnegteq2 (from left to right).
rewrite the current goal using Hm2def (from right to left).
An exact proof term for the current goal is Hmtltm2.
We prove the intermediate claim HltS: apply_fun g i < b.
An exact proof term for the current goal is (add_SNo_Lt1_cancel (apply_fun g i) (minus_SNo xi) b HgiS HmxiS HbS Hineq).
An exact proof term for the current goal is (RltI (apply_fun g i) b HgiR HbR HltS).
We prove the intermediate claim HgiB0: apply_fun g i ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is Hgib.
An exact proof term for the current goal is (Hb0subU (apply_fun g i) HgiB0).
Apply HexBall to the current goal.
Let r0 be given.
Assume Hr0pair.
Apply Hr0pair to the current goal.
Assume Hr0left Hr0sub.
Apply Hr0left to the current goal.
Assume Hr0R Hr0pos.
Set bset to be the term open_ball X d f r0.
We use bset to witness the existential quantifier.
Apply andI to the current goal.
We will prove bset ∈ B.
We prove the intermediate claim HbIn: bset ∈ {open_ball X d f r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr : set ⇒ Rlt 0 r) (λr : set ⇒ open_ball X d f r) r0 Hr0R Hr0pos).
An exact proof term for the current goal is (famunionI X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) f bset HfX HbIn).
Apply andI to the current goal.
We will prove f ∈ bset.
An exact proof term for the current goal is (center_in_open_ball X d f r0 Hm HfX Hr0pos).
An exact proof term for the current goal is Hr0sub.
∎