We will prove R2_dictionary_order_topology = product_topology R (discrete_topology R) R R_standard_topology ∧ R2_dictionary_order_topology ≠ R2_standard_topology.
Apply andI to the current goal.
We prove the intermediate claim Heq: R2_dictionary_order_topology = product_topology R (discrete_topology R) R R_standard_topology.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ R2_dictionary_order_topology.
We will prove U ∈ product_topology R (discrete_topology R) R R_standard_topology.
Set X0 to be the term setprod R R.
Set S to be the term open_rays_subbasis X0.
Set Tprod to be the term product_topology R (discrete_topology R) R R_standard_topology.
We prove the intermediate claim HS: subbasis_on X0 S.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis X0).
We prove the intermediate claim HTx: topology_on R (discrete_topology R).
An exact proof term for the current goal is (discrete_topology_on R).
We prove the intermediate claim HTy: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HTprod: topology_on X0 Tprod.
An exact proof term for the current goal is (product_topology_is_topology R (discrete_topology R) R R_standard_topology HTx HTy).
We prove the intermediate claim HSsub: S ⊆ Tprod.
Let I be given.
Assume HI: I ∈ S.
We will prove I ∈ Tprod.
Apply (binunionE' ({I0 ∈ 𝒫 X0|∃a ∈ X0, I0 = open_ray_upper X0 a} ∪ {I0 ∈ 𝒫 X0|∃b ∈ X0, I0 = open_ray_lower X0 b}) {X0} I (I ∈ Tprod)) to the current goal.
Assume HI0: I ∈ ({I0 ∈ 𝒫 X0|∃a ∈ X0, I0 = open_ray_upper X0 a} ∪ {I0 ∈ 𝒫 X0|∃b ∈ X0, I0 = open_ray_lower X0 b}).
Apply (binunionE' {I0 ∈ 𝒫 X0|∃a ∈ X0, I0 = open_ray_upper X0 a} {I0 ∈ 𝒫 X0|∃b ∈ X0, I0 = open_ray_lower X0 b} I (I ∈ Tprod)) to the current goal.
Assume HIup: I ∈ {I0 ∈ 𝒫 X0|∃a ∈ X0, I0 = open_ray_upper X0 a}.
We prove the intermediate claim Hex: ∃a ∈ X0, I = open_ray_upper X0 a.
An exact proof term for the current goal is (SepE2 (𝒫 X0) (λI0 : set ⇒ ∃a ∈ X0, I0 = open_ray_upper X0 a) I HIup).
Apply Hex to the current goal.
Let a be given.
Assume Hacore.
Apply Hacore to the current goal.
Assume HaX0: a ∈ X0.
Assume HIeq: I = open_ray_upper X0 a.
rewrite the current goal using HIeq (from left to right).
Set a1 to be the term a 0.
Set a2 to be the term a 1.
We prove the intermediate claim Ha1R: a1 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) a HaX0).
We prove the intermediate claim Ha2R: a2 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) a HaX0).
We prove the intermediate claim HaEta: a = (a1,a2).
An exact proof term for the current goal is (setprod_eta R R a HaX0).
Set U0 to be the term open_ray_upper R a1.
Set V0 to be the term open_ray_upper R a2.
Set Rrect to be the term rectangle_set U0 R.
Set Vrect to be the term rectangle_set {a1} V0.
We prove the intermediate claim HU0inTx: U0 ∈ discrete_topology R.
We prove the intermediate claim HdefDisc: discrete_topology R = 𝒫 R.
Use reflexivity.
rewrite the current goal using HdefDisc (from left to right).
We will prove U0 ∈ 𝒫 R.
Apply PowerI to the current goal.
Let x be given.
Assume HxU0: x ∈ U0.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R a1 x0) x HxU0).
We prove the intermediate claim HRinTy: R ∈ R_standard_topology.
An exact proof term for the current goal is (topology_has_X R R_standard_topology HTy).
We prove the intermediate claim HV0inTy: V0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: V0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R a2 Ha2R).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R V0 HsRay).
We prove the intermediate claim Hsing: {a1} ∈ discrete_topology R.
We prove the intermediate claim HdefDisc: discrete_topology R = 𝒫 R.
Use reflexivity.
rewrite the current goal using HdefDisc (from left to right).
Apply PowerI to the current goal.
An exact proof term for the current goal is (singleton_subset a1 R Ha1R).
We prove the intermediate claim Hb1: Rrect ∈ product_subbasis R (discrete_topology R) R R_standard_topology.
We prove the intermediate claim HdefPS: product_subbasis R (discrete_topology R) R R_standard_topology = (⋃U ∈ (discrete_topology R){rectangle_set U V|V ∈ R_standard_topology}).
Use reflexivity.
rewrite the current goal using HdefPS (from left to right).
Apply (famunionI (discrete_topology R) (λU : set ⇒ {rectangle_set U V|V ∈ R_standard_topology}) U0 Rrect HU0inTx) to the current goal.
We will prove Rrect ∈ {rectangle_set U0 V|V ∈ R_standard_topology}.
An exact proof term for the current goal is (ReplI R_standard_topology (λV : set ⇒ rectangle_set U0 V) R HRinTy).
We prove the intermediate claim Hb2: Vrect ∈ product_subbasis R (discrete_topology R) R R_standard_topology.
We prove the intermediate claim HdefPS: product_subbasis R (discrete_topology R) R R_standard_topology = (⋃U ∈ (discrete_topology R){rectangle_set U V|V ∈ R_standard_topology}).
Use reflexivity.
rewrite the current goal using HdefPS (from left to right).
Apply (famunionI (discrete_topology R) (λU : set ⇒ {rectangle_set U V|V ∈ R_standard_topology}) {a1} Vrect Hsing) to the current goal.
We will prove Vrect ∈ {rectangle_set {a1} V|V ∈ R_standard_topology}.
An exact proof term for the current goal is (ReplI R_standard_topology (λV : set ⇒ rectangle_set {a1} V) V0 HV0inTy).
We prove the intermediate claim Hbasis: basis_on X0 (product_subbasis R (discrete_topology R) R R_standard_topology).
An exact proof term for the current goal is (product_subbasis_is_basis R (discrete_topology R) R R_standard_topology HTx HTy).
We prove the intermediate claim Hb1open: Rrect ∈ Tprod.
An exact proof term for the current goal is (generated_topology_contains_basis X0 (product_subbasis R (discrete_topology R) R R_standard_topology) Hbasis Rrect Hb1).
We prove the intermediate claim Hb2open: Vrect ∈ Tprod.
An exact proof term for the current goal is (generated_topology_contains_basis X0 (product_subbasis R (discrete_topology R) R R_standard_topology) Hbasis Vrect Hb2).
We prove the intermediate claim Hop: open_ray_upper X0 a = Rrect ∪ Vrect.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ open_ray_upper X0 a.
We prove the intermediate claim HpX0: p ∈ X0.
An exact proof term for the current goal is (SepE1 X0 (λx0 : set ⇒ order_rel X0 a x0) p Hp).
Set p1 to be the term p 0.
Set p2 to be the term p 1.
We prove the intermediate claim Hp1R: p1 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpX0).
We prove the intermediate claim Hp2R: p2 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpX0).
We prove the intermediate claim HpEta: p = (p1,p2).
An exact proof term for the current goal is (setprod_eta R R p HpX0).
We prove the intermediate claim Hrel: order_rel X0 a p.
An exact proof term for the current goal is (SepE2 X0 (λx0 : set ⇒ order_rel X0 a x0) p Hp).
We prove the intermediate claim Hunf: Rlt a1 p1 ∨ (a1 = p1 ∧ Rlt a2 p2).
We prove the intermediate claim Hrel': order_rel X0 (a1,a2) (p1,p2).
rewrite the current goal using HaEta (from right to left) at position 1.
rewrite the current goal using HpEta (from right to left) at position 1.
An exact proof term for the current goal is Hrel.
Apply (order_rel_setprod_R_R_unfold (a1,a2) (p1,p2) Hrel') to the current goal.
Let c1 be given.
Assume Hc1rest.
Apply Hc1rest to the current goal.
Let c2 be given.
Assume Hc2rest.
Apply Hc2rest to the current goal.
Let d1 be given.
Assume Hd1rest.
Apply Hd1rest to the current goal.
Let d2 be given.
Assume Hpack: ((a1,a2) = (c1,c2) ∧ (p1,p2) = (d1,d2)) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
We prove the intermediate claim Heqs: (a1,a2) = (c1,c2) ∧ (p1,p2) = (d1,d2).
An exact proof term for the current goal is (andEL ((a1,a2) = (c1,c2) ∧ (p1,p2) = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER ((a1,a2) = (c1,c2) ∧ (p1,p2) = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack).
We prove the intermediate claim HacEq: (a1,a2) = (c1,c2).
An exact proof term for the current goal is (andEL ((a1,a2) = (c1,c2)) ((p1,p2) = (d1,d2)) Heqs).
We prove the intermediate claim HpdEq: (p1,p2) = (d1,d2).
An exact proof term for the current goal is (andER ((a1,a2) = (c1,c2)) ((p1,p2) = (d1,d2)) Heqs).
We prove the intermediate claim Hc1eq: c1 = a1.
We prove the intermediate claim Ha1eq: a1 = c1.
rewrite the current goal using (tuple_2_0_eq a1 a2) (from right to left).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left).
rewrite the current goal using HacEq (from left to right).
Use reflexivity.
We will prove c1 = a1.
rewrite the current goal using Ha1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hc2eq: c2 = a2.
We prove the intermediate claim Ha2eq: a2 = c2.
rewrite the current goal using (tuple_2_1_eq a1 a2) (from right to left).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left).
rewrite the current goal using HacEq (from left to right).
Use reflexivity.
We will prove c2 = a2.
rewrite the current goal using Ha2eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = p1.
We prove the intermediate claim Hp1eq: p1 = d1.
rewrite the current goal using (tuple_2_0_eq p1 p2) (from right to left).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left).
rewrite the current goal using HpdEq (from left to right).
Use reflexivity.
We will prove d1 = p1.
rewrite the current goal using Hp1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hd2eq: d2 = p2.
We prove the intermediate claim Hp2eq: p2 = d2.
rewrite the current goal using (tuple_2_1_eq p1 p2) (from right to left).
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left).
rewrite the current goal using HpdEq (from left to right).
Use reflexivity.
We will prove d2 = p2.
rewrite the current goal using Hp2eq (from left to right).
Use reflexivity.
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply orIL to the current goal.
We will prove Rlt a1 p1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Assume Hcore: c1 = d1 ∧ Rlt c2 d2.
Apply orIR to the current goal.
Apply andI to the current goal.
We will prove a1 = p1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hcore).
We will prove Rlt a2 p2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hcore).
Apply Hunf to the current goal.
Assume Hlt: Rlt a1 p1.
Apply binunionI1 to the current goal.
rewrite the current goal using rectangle_set_def (from left to right).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 R p1 p2 (SepI R (λx0 : set ⇒ order_rel R a1 x0) p1 Hp1R (Rlt_implies_order_rel_R a1 p1 (RltI a1 p1 Ha1R Hp1R (RltE_lt a1 p1 Hlt)))) Hp2R).
Assume Hcore: a1 = p1 ∧ Rlt a2 p2.
Apply binunionI2 to the current goal.
We prove the intermediate claim Hpeq: p1 = a1.
rewrite the current goal using (andEL (a1 = p1) (Rlt a2 p2) Hcore) (from right to left).
Use reflexivity.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {a1} V0 a1 p2 (SingI a1) (SepI R (λx0 : set ⇒ order_rel R a2 x0) p2 Hp2R (Rlt_implies_order_rel_R a2 p2 (RltI a2 p2 Ha2R Hp2R (RltE_lt a2 p2 (andER (a1 = p1) (Rlt a2 p2) Hcore)))))).
Let p be given.
Assume Hp: p ∈ Rrect ∪ Vrect.
Apply (binunionE Rrect Vrect p Hp (p ∈ open_ray_upper X0 a)) to the current goal.
Assume HpR: p ∈ Rrect.
Set p1 to be the term p 0.
Set p2 to be the term p 1.
We prove the intermediate claim HpUV: p ∈ setprod U0 R.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HpR.
We prove the intermediate claim HU0subR: U0 ⊆ R.
Let x be given.
Assume Hx: x ∈ U0.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R a1 x0) x Hx).
We prove the intermediate claim HpX0: p ∈ X0.
An exact proof term for the current goal is ((setprod_Subq U0 R R R HU0subR (Subq_ref R)) p HpUV).
We prove the intermediate claim HpEta: p = (p1,p2).
An exact proof term for the current goal is (setprod_eta R R p HpX0).
We prove the intermediate claim HpX0pair: (p1,p2) ∈ X0.
rewrite the current goal using HpEta (from right to left).
An exact proof term for the current goal is HpX0.
We prove the intermediate claim Hp1inU0: p1 ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ R) p HpUV).
We prove the intermediate claim Hp2R: p2 ∈ R.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ R) p HpUV).
We prove the intermediate claim Hrel1: order_rel R a1 p1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a1 x0) p1 Hp1inU0).
We prove the intermediate claim Hlt: Rlt a1 p1.
An exact proof term for the current goal is (order_rel_R_implies_Rlt a1 p1 Hrel1).
We will prove p ∈ open_ray_upper X0 a.
We prove the intermediate claim HdefOR: open_ray_upper X0 a = {x ∈ X0|order_rel X0 a x}.
Use reflexivity.
rewrite the current goal using HdefOR (from left to right).
Apply (SepI X0 (λq : set ⇒ order_rel X0 a q) p HpX0) to the current goal.
We prove the intermediate claim HrelX0: order_rel X0 (a1,a2) (p1,p2).
An exact proof term for the current goal is (order_rel_setprod_R_R_intro a1 a2 p1 p2 (orIL (Rlt a1 p1) (a1 = p1 ∧ Rlt a2 p2) Hlt)).
We will prove order_rel X0 a p.
rewrite the current goal using HaEta (from left to right).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is HrelX0.
Assume HpV: p ∈ Vrect.
Set p1 to be the term p 0.
Set p2 to be the term p 1.
We prove the intermediate claim HpUV: p ∈ setprod {a1} V0.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HpV.
We prove the intermediate claim HV0subR: V0 ⊆ R.
Let x be given.
Assume Hx: x ∈ V0.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R a2 x0) x Hx).
We prove the intermediate claim HpX0: p ∈ X0.
An exact proof term for the current goal is ((setprod_Subq {a1} V0 R R (singleton_subset a1 R Ha1R) HV0subR) p HpUV).
We prove the intermediate claim HpEta: p = (p1,p2).
An exact proof term for the current goal is (setprod_eta R R p HpX0).
We prove the intermediate claim HpX0pair: (p1,p2) ∈ X0.
rewrite the current goal using HpEta (from right to left).
An exact proof term for the current goal is HpX0.
We prove the intermediate claim Hp1eq: p1 = a1.
An exact proof term for the current goal is (SingE a1 p1 (ap0_Sigma {a1} (λ_ : set ⇒ V0) p HpUV)).
We prove the intermediate claim Hp2inV0: p2 ∈ V0.
An exact proof term for the current goal is (ap1_Sigma {a1} (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hrel2: order_rel R a2 p2.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a2 x0) p2 Hp2inV0).
We prove the intermediate claim Hlt2: Rlt a2 p2.
An exact proof term for the current goal is (order_rel_R_implies_Rlt a2 p2 Hrel2).
We prove the intermediate claim Ha1eqp1: a1 = p1.
rewrite the current goal using Hp1eq (from right to left).
Use reflexivity.
We will prove p ∈ open_ray_upper X0 a.
We prove the intermediate claim HdefOR: open_ray_upper X0 a = {x ∈ X0|order_rel X0 a x}.
Use reflexivity.
rewrite the current goal using HdefOR (from left to right).
Apply (SepI X0 (λq : set ⇒ order_rel X0 a q) p HpX0) to the current goal.
We prove the intermediate claim HrelX0: order_rel X0 (a1,a2) (p1,p2).
An exact proof term for the current goal is (order_rel_setprod_R_R_intro a1 a2 p1 p2 (orIR (Rlt a1 p1) (a1 = p1 ∧ Rlt a2 p2) (andI (a1 = p1) (Rlt a2 p2) Ha1eqp1 Hlt2))).
We will prove order_rel X0 a p.
rewrite the current goal using HaEta (from left to right).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is HrelX0.
rewrite the current goal using Hop (from left to right).
An exact proof term for the current goal is (topology_binunion_closed X0 Tprod Rrect Vrect HTprod Hb1open Hb2open).
Assume HIlow: I ∈ {I0 ∈ 𝒫 X0|∃b ∈ X0, I0 = open_ray_lower X0 b}.
We prove the intermediate claim Hex: ∃b ∈ X0, I = open_ray_lower X0 b.
An exact proof term for the current goal is (SepE2 (𝒫 X0) (λI0 : set ⇒ ∃b ∈ X0, I0 = open_ray_lower X0 b) I HIlow).
Apply Hex to the current goal.
Let b be given.
Assume Hbcore.
Apply Hbcore to the current goal.
Assume HbX0: b ∈ X0.
Assume HIeq: I = open_ray_lower X0 b.
rewrite the current goal using HIeq (from left to right).
Set b1 to be the term b 0.
Set b2 to be the term b 1.
We prove the intermediate claim Hb1R: b1 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) b HbX0).
We prove the intermediate claim Hb2R: b2 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) b HbX0).
We prove the intermediate claim HbEta: b = (b1,b2).
An exact proof term for the current goal is (setprod_eta R R b HbX0).
Set U0 to be the term open_ray_lower R b1.
Set V0 to be the term open_ray_lower R b2.
Set Rrect to be the term rectangle_set U0 R.
Set Vrect to be the term rectangle_set {b1} V0.
We prove the intermediate claim HU0inTx: U0 ∈ discrete_topology R.
We prove the intermediate claim HdefDisc: discrete_topology R = 𝒫 R.
Use reflexivity.
rewrite the current goal using HdefDisc (from left to right).
We will prove U0 ∈ 𝒫 R.
Apply PowerI to the current goal.
Let x be given.
Assume HxU0: x ∈ U0.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 b1) x HxU0).
We prove the intermediate claim HRinTy: R ∈ R_standard_topology.
An exact proof term for the current goal is (topology_has_X R R_standard_topology HTy).
We prove the intermediate claim HV0inTy: V0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: V0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R b2 Hb2R).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R V0 HsRay).
We prove the intermediate claim Hsing: {b1} ∈ discrete_topology R.
We prove the intermediate claim HdefDisc: discrete_topology R = 𝒫 R.
Use reflexivity.
rewrite the current goal using HdefDisc (from left to right).
Apply PowerI to the current goal.
An exact proof term for the current goal is (singleton_subset b1 R Hb1R).
We prove the intermediate claim Hb1: Rrect ∈ product_subbasis R (discrete_topology R) R R_standard_topology.
We prove the intermediate claim HdefPS: product_subbasis R (discrete_topology R) R R_standard_topology = (⋃U ∈ (discrete_topology R){rectangle_set U V|V ∈ R_standard_topology}).
Use reflexivity.
rewrite the current goal using HdefPS (from left to right).
Apply (famunionI (discrete_topology R) (λU : set ⇒ {rectangle_set U V|V ∈ R_standard_topology}) U0 Rrect HU0inTx) to the current goal.
We will prove Rrect ∈ {rectangle_set U0 V|V ∈ R_standard_topology}.
An exact proof term for the current goal is (ReplI R_standard_topology (λV : set ⇒ rectangle_set U0 V) R HRinTy).
We prove the intermediate claim Hb2: Vrect ∈ product_subbasis R (discrete_topology R) R R_standard_topology.
We prove the intermediate claim HdefPS: product_subbasis R (discrete_topology R) R R_standard_topology = (⋃U ∈ (discrete_topology R){rectangle_set U V|V ∈ R_standard_topology}).
Use reflexivity.
rewrite the current goal using HdefPS (from left to right).
Apply (famunionI (discrete_topology R) (λU : set ⇒ {rectangle_set U V|V ∈ R_standard_topology}) {b1} Vrect Hsing) to the current goal.
We will prove Vrect ∈ {rectangle_set {b1} V|V ∈ R_standard_topology}.
An exact proof term for the current goal is (ReplI R_standard_topology (λV : set ⇒ rectangle_set {b1} V) V0 HV0inTy).
We prove the intermediate claim Hbasis: basis_on X0 (product_subbasis R (discrete_topology R) R R_standard_topology).
An exact proof term for the current goal is (product_subbasis_is_basis R (discrete_topology R) R R_standard_topology HTx HTy).
We prove the intermediate claim Hb1open: Rrect ∈ Tprod.
An exact proof term for the current goal is (generated_topology_contains_basis X0 (product_subbasis R (discrete_topology R) R R_standard_topology) Hbasis Rrect Hb1).
We prove the intermediate claim Hb2open: Vrect ∈ Tprod.
An exact proof term for the current goal is (generated_topology_contains_basis X0 (product_subbasis R (discrete_topology R) R R_standard_topology) Hbasis Vrect Hb2).
We prove the intermediate claim Hop: open_ray_lower X0 b = Rrect ∪ Vrect.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ open_ray_lower X0 b.
We prove the intermediate claim HpX0: p ∈ X0.
An exact proof term for the current goal is (SepE1 X0 (λx0 : set ⇒ order_rel X0 x0 b) p Hp).
Set p1 to be the term p 0.
Set p2 to be the term p 1.
We prove the intermediate claim Hp1R: p1 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpX0).
We prove the intermediate claim Hp2R: p2 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpX0).
We prove the intermediate claim HpEta: p = (p1,p2).
An exact proof term for the current goal is (setprod_eta R R p HpX0).
We prove the intermediate claim Hrel: order_rel X0 p b.
An exact proof term for the current goal is (SepE2 X0 (λx0 : set ⇒ order_rel X0 x0 b) p Hp).
We prove the intermediate claim Hunf: Rlt p1 b1 ∨ (p1 = b1 ∧ Rlt p2 b2).
We prove the intermediate claim Hrel': order_rel X0 (p1,p2) (b1,b2).
rewrite the current goal using HpEta (from right to left) at position 1.
rewrite the current goal using HbEta (from right to left) at position 1.
An exact proof term for the current goal is Hrel.
Apply (order_rel_setprod_R_R_unfold (p1,p2) (b1,b2) Hrel') to the current goal.
Let c1 be given.
Assume Hc1rest.
Apply Hc1rest to the current goal.
Let c2 be given.
Assume Hc2rest.
Apply Hc2rest to the current goal.
Let d1 be given.
Assume Hd1rest.
Apply Hd1rest to the current goal.
Let d2 be given.
Assume Hpack: ((p1,p2) = (c1,c2) ∧ (b1,b2) = (d1,d2)) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).
We prove the intermediate claim Heqs: (p1,p2) = (c1,c2) ∧ (b1,b2) = (d1,d2).
An exact proof term for the current goal is (andEL ((p1,p2) = (c1,c2) ∧ (b1,b2) = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack).
We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).
An exact proof term for the current goal is (andER ((p1,p2) = (c1,c2) ∧ (b1,b2) = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack).
We prove the intermediate claim HpcEq: (p1,p2) = (c1,c2).
An exact proof term for the current goal is (andEL ((p1,p2) = (c1,c2)) ((b1,b2) = (d1,d2)) Heqs).
We prove the intermediate claim HbdEq: (b1,b2) = (d1,d2).
An exact proof term for the current goal is (andER ((p1,p2) = (c1,c2)) ((b1,b2) = (d1,d2)) Heqs).
We prove the intermediate claim Hc1eq: c1 = p1.
We prove the intermediate claim Hp1eq: p1 = c1.
rewrite the current goal using (tuple_2_0_eq p1 p2) (from right to left).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left).
rewrite the current goal using HpcEq (from left to right).
Use reflexivity.
We will prove c1 = p1.
rewrite the current goal using Hp1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hc2eq: c2 = p2.
We prove the intermediate claim Hp2eq: p2 = c2.
rewrite the current goal using (tuple_2_1_eq p1 p2) (from right to left).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left).
rewrite the current goal using HpcEq (from left to right).
Use reflexivity.
We will prove c2 = p2.
rewrite the current goal using Hp2eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hd1eq: d1 = b1.
We prove the intermediate claim Hb1eq: b1 = d1.
rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).
rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left).
rewrite the current goal using HbdEq (from left to right).
Use reflexivity.
We will prove d1 = b1.
rewrite the current goal using Hb1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hd2eq: d2 = b2.
We prove the intermediate claim Hb2eq: b2 = d2.
rewrite the current goal using (tuple_2_1_eq b1 b2) (from right to left).
rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left).
rewrite the current goal using HbdEq (from left to right).
Use reflexivity.
We will prove d2 = b2.
rewrite the current goal using Hb2eq (from left to right).
Use reflexivity.
Apply Hdisj to the current goal.
Assume Hlt: Rlt c1 d1.
Apply orIL to the current goal.
We will prove Rlt p1 b1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
Assume Hcore: c1 = d1 ∧ Rlt c2 d2.
Apply orIR to the current goal.
Apply andI to the current goal.
We will prove p1 = b1.
rewrite the current goal using Hc1eq (from right to left) at position 1.
rewrite the current goal using Hd1eq (from right to left) at position 1.
An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hcore).
We will prove Rlt p2 b2.
rewrite the current goal using Hc2eq (from right to left) at position 1.
rewrite the current goal using Hd2eq (from right to left) at position 1.
An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hcore).
Apply Hunf to the current goal.
Assume Hlt: Rlt p1 b1.
Apply binunionI1 to the current goal.
rewrite the current goal using rectangle_set_def (from left to right).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 R p1 p2 (SepI R (λx0 : set ⇒ order_rel R x0 b1) p1 Hp1R (Rlt_implies_order_rel_R p1 b1 (RltI p1 b1 Hp1R Hb1R (RltE_lt p1 b1 Hlt)))) Hp2R).
Assume Hcore: p1 = b1 ∧ Rlt p2 b2.
Apply binunionI2 to the current goal.
We prove the intermediate claim Hpeq: p1 = b1.
An exact proof term for the current goal is (andEL (p1 = b1) (Rlt p2 b2) Hcore).
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {b1} V0 b1 p2 (SingI b1) (SepI R (λx0 : set ⇒ order_rel R x0 b2) p2 Hp2R (Rlt_implies_order_rel_R p2 b2 (RltI p2 b2 Hp2R Hb2R (RltE_lt p2 b2 (andER (p1 = b1) (Rlt p2 b2) Hcore)))))).
Let p be given.
Assume Hp: p ∈ Rrect ∪ Vrect.
Apply (binunionE Rrect Vrect p Hp (p ∈ open_ray_lower X0 b)) to the current goal.
Assume HpR: p ∈ Rrect.
Set p1 to be the term p 0.
Set p2 to be the term p 1.
We prove the intermediate claim HpUV: p ∈ setprod U0 R.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HpR.
We prove the intermediate claim HU0subR: U0 ⊆ R.
Let x be given.
Assume Hx: x ∈ U0.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 b1) x Hx).
We prove the intermediate claim HpX0: p ∈ X0.
An exact proof term for the current goal is ((setprod_Subq U0 R R R HU0subR (Subq_ref R)) p HpUV).
We prove the intermediate claim HpEta: p = (p1,p2).
An exact proof term for the current goal is (setprod_eta R R p HpX0).
We prove the intermediate claim Hp1inU0: p1 ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ R) p HpUV).
We prove the intermediate claim Hrel1: order_rel R p1 b1.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b1) p1 Hp1inU0).
We prove the intermediate claim Hlt: Rlt p1 b1.
An exact proof term for the current goal is (order_rel_R_implies_Rlt p1 b1 Hrel1).
We will prove p ∈ open_ray_lower X0 b.
We prove the intermediate claim HdefOL: open_ray_lower X0 b = {x ∈ X0|order_rel X0 x b}.
Use reflexivity.
rewrite the current goal using HdefOL (from left to right).
Apply (SepI X0 (λq : set ⇒ order_rel X0 q b) p HpX0) to the current goal.
We prove the intermediate claim HrelX0: order_rel X0 (p1,p2) (b1,b2).
An exact proof term for the current goal is (order_rel_setprod_R_R_intro p1 p2 b1 b2 (orIL (Rlt p1 b1) (p1 = b1 ∧ Rlt p2 b2) Hlt)).
We will prove order_rel X0 p b.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using HbEta (from left to right).
An exact proof term for the current goal is HrelX0.
Assume HpV: p ∈ Vrect.
Set p1 to be the term p 0.
Set p2 to be the term p 1.
We prove the intermediate claim HpUV: p ∈ setprod {b1} V0.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HpV.
We prove the intermediate claim HV0subR: V0 ⊆ R.
Let x be given.
Assume Hx: x ∈ V0.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 b2) x Hx).
We prove the intermediate claim HpX0: p ∈ X0.
An exact proof term for the current goal is ((setprod_Subq {b1} V0 R R (singleton_subset b1 R Hb1R) HV0subR) p HpUV).
We prove the intermediate claim HpEta: p = (p1,p2).
An exact proof term for the current goal is (setprod_eta R R p HpX0).
We prove the intermediate claim Hp1eq: p1 = b1.
An exact proof term for the current goal is (SingE b1 p1 (ap0_Sigma {b1} (λ_ : set ⇒ V0) p HpUV)).
We prove the intermediate claim Hp2inV0: p2 ∈ V0.
An exact proof term for the current goal is (ap1_Sigma {b1} (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hrel2: order_rel R p2 b2.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b2) p2 Hp2inV0).
We prove the intermediate claim Hlt2: Rlt p2 b2.
An exact proof term for the current goal is (order_rel_R_implies_Rlt p2 b2 Hrel2).
We prove the intermediate claim Hp1eq2: p1 = b1.
An exact proof term for the current goal is Hp1eq.
We will prove p ∈ open_ray_lower X0 b.
We prove the intermediate claim HdefOL: open_ray_lower X0 b = {x ∈ X0|order_rel X0 x b}.
Use reflexivity.
rewrite the current goal using HdefOL (from left to right).
Apply (SepI X0 (λq : set ⇒ order_rel X0 q b) p HpX0) to the current goal.
We prove the intermediate claim HrelX0: order_rel X0 (p1,p2) (b1,b2).
An exact proof term for the current goal is (order_rel_setprod_R_R_intro p1 p2 b1 b2 (orIR (Rlt p1 b1) (p1 = b1 ∧ Rlt p2 b2) (andI (p1 = b1) (Rlt p2 b2) Hp1eq2 Hlt2))).
We will prove order_rel X0 p b.
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using HbEta (from left to right).
An exact proof term for the current goal is HrelX0.
rewrite the current goal using Hop (from left to right).
An exact proof term for the current goal is (topology_binunion_closed X0 Tprod Rrect Vrect HTprod Hb1open Hb2open).
An exact proof term for the current goal is HI0.
Assume HIX: I ∈ {X0}.
We prove the intermediate claim HIeq: I = X0.
An exact proof term for the current goal is (SingE X0 I HIX).
rewrite the current goal using HIeq (from left to right).
An exact proof term for the current goal is (topology_has_X X0 Tprod HTprod).
An exact proof term for the current goal is HI.
We prove the intermediate claim Hmin: finer_than Tprod (generated_topology_from_subbasis X0 S).
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal X0 S Tprod HS HTprod HSsub).
An exact proof term for the current goal is (Hmin U HU).
Let U be given.
Assume HU: U ∈ product_topology R (discrete_topology R) R R_standard_topology.
We will prove U ∈ R2_dictionary_order_topology.
Set X0 to be the term setprod R R.
Set B to be the term product_subbasis R (discrete_topology R) R R_standard_topology.
Set Tprod to be the term product_topology R (discrete_topology R) R R_standard_topology.
Set T to be the term R2_dictionary_order_topology.
We prove the intermediate claim HTx: topology_on R (discrete_topology R).
An exact proof term for the current goal is (discrete_topology_on R).
We prove the intermediate claim HTy: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HBasis: basis_on X0 B.
An exact proof term for the current goal is (product_subbasis_is_basis R (discrete_topology R) R R_standard_topology HTx HTy).
We prove the intermediate claim HTprod: topology_on X0 Tprod.
An exact proof term for the current goal is (lemma_topology_from_basis X0 B HBasis).
We prove the intermediate claim HUopen: open_in X0 Tprod U.
An exact proof term for the current goal is (andI (topology_on X0 Tprod) (U ∈ Tprod) HTprod HU).
We prove the intermediate claim HexFam: ∃Fam ∈ 𝒫 B, ⋃ Fam = U.
An exact proof term for the current goal is (open_sets_as_unions_of_basis X0 B HBasis U HUopen).
Apply HexFam to the current goal.
Let Fam be given.
Assume HFcore.
Apply HFcore to the current goal.
Assume HFamPow: Fam ∈ 𝒫 B.
Assume HUnionEq: ⋃ Fam = U.
rewrite the current goal using HUnionEq (from right to left).
We prove the intermediate claim HT: topology_on X0 T.
An exact proof term for the current goal is dictionary_order_topology_is_topology.
Apply (topology_union_closed_pow X0 T Fam HT) to the current goal.
Apply PowerI to the current goal.
Let I be given.
Assume HI: I ∈ Fam.
We prove the intermediate claim HIb: I ∈ B.
An exact proof term for the current goal is (PowerE B Fam HFamPow I HI).
Apply (famunionE_impred (discrete_topology R) (λU0 : set ⇒ {rectangle_set U0 V|V ∈ R_standard_topology}) I HIb (I ∈ T)) to the current goal.
Let U0 be given.
Assume HU0Tx HIU0.
Apply (ReplE_impred R_standard_topology (λV0 : set ⇒ rectangle_set U0 V0) I HIU0 (I ∈ T)) to the current goal.
Let V0 be given.
Assume HV0Ty HIeq.
rewrite the current goal using HIeq (from left to right).
An exact proof term for the current goal is (rectangle_in_dictionary U0 V0 HU0Tx HV0Ty).
An exact proof term for the current goal is Heq.
We will prove R2_dictionary_order_topology ≠ R2_standard_topology.
Assume HeqTop: R2_dictionary_order_topology = R2_standard_topology.
Apply FalseE to the current goal.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim H01: Rlt 0 1.
An exact proof term for the current goal is (RltI 0 1 H0R H1R SNoLt_0_1).
Set V to be the term open_interval 0 1.
Set U to be the term rectangle_set {0} V.
We prove the intermediate claim HV: V ∈ R_standard_topology.
An exact proof term for the current goal is (open_interval_in_R_standard_topology 0 1 H01).
We prove the intermediate claim HUdict: U ∈ R2_dictionary_order_topology.
An exact proof term for the current goal is (singleton_rectangle_in_dictionary 0 V H0R HV).
We prove the intermediate claim HUstd: U ∈ R2_standard_topology.
rewrite the current goal using HeqTop (from right to left).
An exact proof term for the current goal is HUdict.
We prove the intermediate claim HUnot: U ∉ R2_standard_topology.
Assume HU: U ∈ R2_standard_topology.
We will prove False.
Set X0 to be the term setprod R R.
Set B to be the term product_subbasis R R_standard_topology R R_standard_topology.
We prove the intermediate claim HTx: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HTy: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HBasis: basis_on X0 B.
An exact proof term for the current goal is (product_subbasis_is_basis R R_standard_topology R R_standard_topology HTx HTy).
We prove the intermediate claim HTstd: topology_on X0 R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology HTx HTy).
We prove the intermediate claim HUopen: open_in X0 R2_standard_topology U.
An exact proof term for the current goal is (andI (topology_on X0 R2_standard_topology) (U ∈ R2_standard_topology) HTstd HU).
We prove the intermediate claim HexFam: ∃Fam ∈ 𝒫 B, ⋃ Fam = U.
An exact proof term for the current goal is (open_sets_as_unions_of_basis X0 B HBasis U HUopen).
Apply HexFam to the current goal.
Let Fam be given.
Assume HFcore.
Apply HFcore to the current goal.
Assume HFamPow: Fam ∈ 𝒫 B.
Assume HUnionEq: ⋃ Fam = U.
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt 0 q ∧ Rlt q 1.
An exact proof term for the current goal is (rational_dense_between_reals 0 1 H0R H1R H01).
Apply Hexq to the current goal.
Let q be given.
Assume Hqcore.
Apply Hqcore to the current goal.
Assume HqQ Hqineq.
We prove the intermediate claim H0q: Rlt 0 q.
An exact proof term for the current goal is (andEL (Rlt 0 q) (Rlt q 1) Hqineq).
We prove the intermediate claim Hq1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt 0 q) (Rlt q 1) Hqineq).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HqV: q ∈ V.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt 0 z ∧ Rlt z 1) q HqR (andI (Rlt 0 q) (Rlt q 1) H0q Hq1)).
Set p to be the term (0,q).
We prove the intermediate claim HpU: p ∈ U.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {0} V 0 q (SingI 0) HqV).
We prove the intermediate claim HpUnion: p ∈ ⋃ Fam.
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HpU.
Apply (UnionE_impred Fam p HpUnion False) to the current goal.
Let I be given.
Assume HpI HIinFam.
We prove the intermediate claim HIb: I ∈ B.
An exact proof term for the current goal is (PowerE B Fam HFamPow I HIinFam).
Apply (famunionE_impred R_standard_topology (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ R_standard_topology}) I HIb False) to the current goal.
Let U0 be given.
Assume HU0open HIU0.
Apply (ReplE_impred R_standard_topology (λV0 : set ⇒ rectangle_set U0 V0) I HIU0 False) to the current goal.
Let V0 be given.
Assume HV0open HIeq.
We prove the intermediate claim HpUV: p ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HpI.
We prove the intermediate claim Hp0U0: p 0 ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hp1V0: p 1 ∈ V0.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hp0eq: p 0 = 0.
An exact proof term for the current goal is (tuple_2_0_eq 0 q).
We prove the intermediate claim Hp1eq: p 1 = q.
An exact proof term for the current goal is (tuple_2_1_eq 0 q).
We prove the intermediate claim H0U0: 0 ∈ U0.
rewrite the current goal using Hp0eq (from right to left).
An exact proof term for the current goal is Hp0U0.
We prove the intermediate claim HqV0: q ∈ V0.
rewrite the current goal using Hp1eq (from right to left).
An exact proof term for the current goal is Hp1V0.
We prove the intermediate claim HU0sub: U0 ⊆ {0}.
Let x be given.
Assume Hx: x ∈ U0.
We prove the intermediate claim HxqUV: (x,q) ∈ setprod U0 V0.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 V0 x q Hx HqV0).
We prove the intermediate claim HxqI: (x,q) ∈ I.
rewrite the current goal using HIeq (from left to right).
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is HxqUV.
We prove the intermediate claim HxqUnion: (x,q) ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam (x,q) I HxqI HIinFam).
We prove the intermediate claim HxqU: (x,q) ∈ U.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HxqUnion.
We prove the intermediate claim HxqUS: (x,q) ∈ setprod {0} V.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is HxqU.
We prove the intermediate claim Hx0: (x,q) 0 ∈ {0}.
An exact proof term for the current goal is (ap0_Sigma {0} (λ_ : set ⇒ V) (x,q) HxqUS).
rewrite the current goal using (tuple_2_0_eq x q) (from right to left).
An exact proof term for the current goal is Hx0.
We prove the intermediate claim HsingSub: {0} ⊆ U0.
Let y be given.
Assume Hy: y ∈ {0}.
We prove the intermediate claim Hyeq: y = 0.
An exact proof term for the current goal is (SingE 0 y Hy).
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is H0U0.
We prove the intermediate claim HU0eq: U0 = {0}.
Apply set_ext to the current goal.
An exact proof term for the current goal is HU0sub.
An exact proof term for the current goal is HsingSub.
We prove the intermediate claim HsingOpen: {0} ∈ R_standard_topology.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HU0open.
An exact proof term for the current goal is (singleton_not_open_R_standard_topology 0 H0R HsingOpen).
Apply HUnot to the current goal.
An exact proof term for the current goal is HUstd.
∎