Assume Hcr: completely_regular_space X Tx.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (andEL (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1) Hcr).

We prove the intermediate claim Hrest: one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.

An exact proof term for the current goal is (andER (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1) Hcr).

We prove the intermediate claim HT1: one_point_sets_closed X Tx.

An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1) Hrest).

Set J to be the term {f ∈ function_space X unit_interval|continuous_map X Tx unit_interval unit_interval_topology f}.

Set F to be the term graph J (λf : set ⇒ f).

Set Fmap to be the term diagonal_map X F J.

We use J to witness the existential quantifier.

We use Fmap to witness the existential quantifier.

Set Xi to be the term const_space_family J unit_interval unit_interval_topology.

We prove the intermediate claim HTyEq: product_topology_full J (const_space_family J unit_interval (subspace_topology R R_standard_topology unit_interval)) = product_topology_full J Xi.

Use reflexivity.

rewrite the current goal using HTyEq (from left to right).

Set Ty to be the term product_topology_full J Xi.

We prove the intermediate claim HJne: J ≠ Empty.

We prove the intermediate claim H0I: 0 ∈ unit_interval.

An exact proof term for the current goal is zero_in_unit_interval.

We prove the intermediate claim HTui: topology_on unit_interval unit_interval_topology.

An exact proof term for the current goal is unit_interval_topology_on.

We prove the intermediate claim HconstCont: continuous_map X Tx unit_interval unit_interval_topology (const_fun X 0).

An exact proof term for the current goal is (const_fun_continuous X Tx unit_interval unit_interval_topology 0 HTx HTui H0I).

We prove the intermediate claim HconstFS: const_fun X 0 ∈ function_space X unit_interval.

Set f0 to be the term const_fun X 0.

We prove the intermediate claim Hsub: f0 ⊆ setprod X unit_interval.

Let q be given.

Assume Hq: q ∈ f0.

We will prove q ∈ setprod X unit_interval.

Apply (ReplE_impred X (λa0 : set ⇒ (a0,0)) q Hq (q ∈ setprod X unit_interval)) to the current goal.

Let a be given.

Assume HaX: a ∈ X.

Assume Heq: q = (a,0).

rewrite the current goal using Heq (from left to right).

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X unit_interval a 0 HaX H0I).

We prove the intermediate claim Hpow: f0 ∈ 𝒫 (setprod X unit_interval).

An exact proof term for the current goal is (PowerI (setprod X unit_interval) f0 Hsub).

We prove the intermediate claim Hfun: function_on f0 X unit_interval.

Let x be given.

Assume HxX: x ∈ X.

We will prove apply_fun f0 x ∈ unit_interval.

We prove the intermediate claim Happ: apply_fun f0 x = 0.

An exact proof term for the current goal is (const_fun_apply X 0 x HxX).

rewrite the current goal using Happ (from left to right).

An exact proof term for the current goal is H0I.

An exact proof term for the current goal is (SepI (𝒫 (setprod X unit_interval)) (λf0 : set ⇒ function_on f0 X unit_interval) f0 Hpow Hfun).

We prove the intermediate claim HconstJ: const_fun X 0 ∈ J.

Apply (SepI (function_space X unit_interval) (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0) (const_fun X 0) HconstFS HconstCont) to the current goal.

Assume HJ0: J = Empty.

We prove the intermediate claim Hbad: const_fun X 0 ∈ Empty.

rewrite the current goal using HJ0 (from right to left) at position 2.

An exact proof term for the current goal is HconstJ.

An exact proof term for the current goal is (EmptyE (const_fun X 0) Hbad).

We prove the intermediate claim HtotF: total_function_on F J (function_space X unit_interval).

We prove the intermediate claim HFdef: F = graph J (λf0 : set ⇒ f0).

Use reflexivity.

rewrite the current goal using HFdef (from left to right).

Apply (total_function_on_graph J (function_space X unit_interval) (λf0 : set ⇒ f0)) to the current goal.

Let f0 be given.

Assume HfJ: f0 ∈ J.

An exact proof term for the current goal is (SepE1 (function_space X unit_interval) (λf1 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f1) f0 HfJ).

We prove the intermediate claim HcoordCont: ∀j : set, j ∈ J → continuous_map X Tx unit_interval unit_interval_topology (apply_fun F j).

Let j be given.

Assume HjJ: j ∈ J.

We prove the intermediate claim HFdef: F = graph J (λf0 : set ⇒ f0).

Use reflexivity.

rewrite the current goal using HFdef (from left to right).

rewrite the current goal using (apply_fun_graph J (λf0 : set ⇒ f0) j HjJ) (from left to right).

An exact proof term for the current goal is (SepE2 (function_space X unit_interval) (λf1 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f1) j HjJ).

We prove the intermediate claim HcontFmap: continuous_map X Tx (unit_interval_power J) (product_topology_full J Xi) Fmap.

An exact proof term for the current goal is (diagonal_map_continuous_unit_interval_power X Tx F J HTx HJne HtotF HcoordCont).

We prove the intermediate claim Hloc: ∀x U : set, x ∈ X → U ∈ Tx → x ∈ U → ∃V : set, V ∈ (product_topology_full J Xi) ∧ apply_fun Fmap x ∈ V ∧ preimage_of X Fmap V ⊆ U.

Let x and U be given.

Assume HxX: x ∈ X.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We prove the intermediate claim Hexh: ∃h : set, h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h ∧ apply_fun h x = 1 ∧ ∀y : set, y ∈ X ∖ U → apply_fun h y = 0.

An exact proof term for the current goal is (completely_regular_space_open_separator_unit_interval_in_function_space X Tx x U Hcr HxX HU HxU).

Apply Hexh to the current goal.

Let h be given.

Assume Hhpack: h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h ∧ apply_fun h x = 1 ∧ ∀y : set, y ∈ X ∖ U → apply_fun h y = 0.

We prove the intermediate claim Hhpair: (h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) ∧ apply_fun h x = 1.

An exact proof term for the current goal is (andEL ((h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) ∧ apply_fun h x = 1) (∀y : set, y ∈ X ∖ U → apply_fun h y = 0) Hhpack).

We prove the intermediate claim Hhzero: ∀y : set, y ∈ X ∖ U → apply_fun h y = 0.

An exact proof term for the current goal is (andER ((h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) ∧ apply_fun h x = 1) (∀y : set, y ∈ X ∖ U → apply_fun h y = 0) Hhpack).

We prove the intermediate claim Hhpair2: h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h.

An exact proof term for the current goal is (andEL (h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) (apply_fun h x = 1) Hhpair).

We prove the intermediate claim HhFS: h ∈ function_space X unit_interval.

An exact proof term for the current goal is (andEL (h ∈ function_space X unit_interval) (continuous_map X Tx unit_interval unit_interval_topology h) Hhpair2).

We prove the intermediate claim Hhcont: continuous_map X Tx unit_interval unit_interval_topology h.

An exact proof term for the current goal is (andER (h ∈ function_space X unit_interval) (continuous_map X Tx unit_interval unit_interval_topology h) Hhpair2).

We prove the intermediate claim Hhx1: apply_fun h x = 1.

An exact proof term for the current goal is (andER (h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) (apply_fun h x = 1) Hhpair).

We prove the intermediate claim HhJ: h ∈ J.

An exact proof term for the current goal is (SepI (function_space X unit_interval) (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0) h HhFS Hhcont).

Set V0 to be the term (open_interval 0 2) ∩ unit_interval.

We prove the intermediate claim HV0openR: open_interval 0 2 ∈ R_standard_topology.

We prove the intermediate claim HRlt02: Rlt 0 2.

An exact proof term for the current goal is (RltI 0 2 real_0 real_2 SNoLt_0_2).

An exact proof term for the current goal is (open_interval_in_R_standard_topology 0 2 HRlt02).

We prove the intermediate claim HV0: V0 ∈ unit_interval_topology.

An exact proof term for the current goal is (subspace_topologyI R R_standard_topology unit_interval (open_interval 0 2) HV0openR).

Set V to be the term product_cylinder J Xi h V0.

We prove the intermediate claim HXiTop: ∀i0 : set, i0 ∈ J → topology_on (space_family_set Xi i0) (space_family_topology Xi i0).

Let i0 be given.

Assume Hi0J: i0 ∈ J.

We will prove topology_on (space_family_set Xi i0) (space_family_topology Xi i0).

rewrite the current goal using (space_family_set_const_space_family J unit_interval unit_interval_topology i0 Hi0J) (from left to right).

rewrite the current goal using (space_family_topology_const_space_family J unit_interval unit_interval_topology i0 Hi0J) (from left to right).

An exact proof term for the current goal is unit_interval_topology_on.

We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).

An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HJne HXiTop).

We use V to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HVsub: V ∈ product_subbasis_full J Xi.

Set Fam to be the term (λj0 : set ⇒ {product_cylinder J Xi j0 U0|U0 ∈ space_family_topology Xi j0}).

We prove the intermediate claim HV0top: V0 ∈ space_family_topology Xi h.

rewrite the current goal using (space_family_topology_const_space_family J unit_interval unit_interval_topology h HhJ) (from left to right).

An exact proof term for the current goal is HV0.

We prove the intermediate claim HVFam: V ∈ Fam h.

An exact proof term for the current goal is (ReplI (space_family_topology Xi h) (λU0 : set ⇒ product_cylinder J Xi h U0) V0 HV0top).

An exact proof term for the current goal is (famunionI J Fam h V HhJ HVFam).

An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem (product_space J Xi) (product_subbasis_full J Xi) V HSsub HVsub).

We prove the intermediate claim HYdef: unit_interval_power J = product_space J Xi.

Use reflexivity.

We prove the intermediate claim HfunPow0: function_on Fmap X (unit_interval_power J).

An exact proof term for the current goal is (diagonal_map_function_on_unit_interval_power X F J HtotF).

We prove the intermediate claim HfunPow: function_on Fmap X (product_space J Xi).

rewrite the current goal using HYdef (from right to left).

An exact proof term for the current goal is HfunPow0.

We prove the intermediate claim HFmapxY: apply_fun Fmap x ∈ product_space J Xi.

An exact proof term for the current goal is (HfunPow x HxX).

We prove the intermediate claim HcylDef: product_cylinder J Xi h V0 = {f0 ∈ product_space J Xi|h ∈ J ∧ V0 ∈ space_family_topology Xi h ∧ apply_fun f0 h ∈ V0}.

Use reflexivity.

rewrite the current goal using HcylDef (from left to right).

Apply (SepI (product_space J Xi) (λf0 : set ⇒ h ∈ J ∧ V0 ∈ space_family_topology Xi h ∧ apply_fun f0 h ∈ V0) (apply_fun Fmap x) HFmapxY) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is HhJ.

We prove the intermediate claim HV0top: V0 ∈ space_family_topology Xi h.

rewrite the current goal using (space_family_topology_const_space_family J unit_interval unit_interval_topology h HhJ) (from left to right).

An exact proof term for the current goal is HV0.

An exact proof term for the current goal is HV0top.

We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x) h = apply_fun h x.

rewrite the current goal using (diagonal_map_coord_apply X F J x h HxX HhJ) (from left to right).

We prove the intermediate claim HFdef: F = graph J (λf0 : set ⇒ f0).

Use reflexivity.

rewrite the current goal using HFdef (from left to right).

rewrite the current goal using (apply_fun_graph J (λf0 : set ⇒ f0) h HhJ) (from left to right).

Use reflexivity.

We prove the intermediate claim H1V0: 1 ∈ V0.

Apply (binintersectI (open_interval 0 2) unit_interval 1) to the current goal.

We prove the intermediate claim HdefOI: open_interval 0 2 = {t ∈ R|Rlt 0 t ∧ Rlt t 2}.

Use reflexivity.

rewrite the current goal using HdefOI (from left to right).

We prove the intermediate claim H1R: 1 ∈ R.

We prove the intermediate claim HRdef: R = real.

Use reflexivity.

rewrite the current goal using HRdef (from left to right).

An exact proof term for the current goal is real_1.

Apply (SepI R (λt : set ⇒ Rlt 0 t ∧ Rlt t 2) 1 H1R) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is (RltI 0 1 real_0 real_1 SNoLt_0_1).

An exact proof term for the current goal is (RltI 1 2 real_1 real_2 SNoLt_1_2).

An exact proof term for the current goal is one_in_unit_interval.

rewrite the current goal using HcoordEq (from left to right).

rewrite the current goal using Hhx1 (from left to right).

An exact proof term for the current goal is H1V0.

Let y be given.

Assume HyPre: y ∈ preimage_of X Fmap V.

We will prove y ∈ U.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ apply_fun Fmap y0 ∈ V) y HyPre).

We prove the intermediate claim HFmapyV: apply_fun Fmap y ∈ V.

An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ apply_fun Fmap y0 ∈ V) y HyPre).

Apply (xm (y ∈ U)) to the current goal.

Assume HyU: y ∈ U.

An exact proof term for the current goal is HyU.

Assume HyNotU: y ∉ U.

Apply FalseE to the current goal.

We will prove False.

We prove the intermediate claim HyOut: y ∈ X ∖ U.

An exact proof term for the current goal is (setminusI X U y HyX HyNotU).

We prove the intermediate claim Hhy0: apply_fun h y = 0.

An exact proof term for the current goal is (Hhzero y HyOut).

We prove the intermediate claim HcylDef: product_cylinder J Xi h V0 = {f0 ∈ product_space J Xi|h ∈ J ∧ V0 ∈ space_family_topology Xi h ∧ apply_fun f0 h ∈ V0}.

Use reflexivity.

We prove the intermediate claim HFmapyCyl: apply_fun Fmap y ∈ product_cylinder J Xi h V0.

An exact proof term for the current goal is HFmapyV.

We prove the intermediate claim HFmapyCyl2: apply_fun Fmap y ∈ {f0 ∈ product_space J Xi|h ∈ J ∧ V0 ∈ space_family_topology Xi h ∧ apply_fun f0 h ∈ V0}.

rewrite the current goal using HcylDef (from right to left).

An exact proof term for the current goal is HFmapyCyl.

We prove the intermediate claim HyProp: h ∈ J ∧ V0 ∈ space_family_topology Xi h ∧ apply_fun (apply_fun Fmap y) h ∈ V0.

An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf0 : set ⇒ h ∈ J ∧ V0 ∈ space_family_topology Xi h ∧ apply_fun f0 h ∈ V0) (apply_fun Fmap y) HFmapyCyl2).

We prove the intermediate claim HcoordIn: apply_fun (apply_fun Fmap y) h ∈ V0.

An exact proof term for the current goal is (andER (h ∈ J ∧ V0 ∈ space_family_topology Xi h) (apply_fun (apply_fun Fmap y) h ∈ V0) HyProp).

We prove the intermediate claim HcoordEqy: apply_fun (apply_fun Fmap y) h = apply_fun h y.

rewrite the current goal using (diagonal_map_coord_apply X F J y h HyX HhJ) (from left to right).

We prove the intermediate claim HFdef: F = graph J (λf0 : set ⇒ f0).

Use reflexivity.

rewrite the current goal using HFdef (from left to right).

rewrite the current goal using (apply_fun_graph J (λf0 : set ⇒ f0) h HhJ) (from left to right).

Use reflexivity.

We prove the intermediate claim H0V0: 0 ∈ V0.

rewrite the current goal using Hhy0 (from right to left) at position 1.

rewrite the current goal using HcoordEqy (from right to left) at position 1.

An exact proof term for the current goal is HcoordIn.

We prove the intermediate claim H0open: 0 ∈ open_interval 0 2.

An exact proof term for the current goal is (binintersectE1 (open_interval 0 2) unit_interval 0 H0V0).

We prove the intermediate claim HdefOI: open_interval 0 2 = {t ∈ R|Rlt 0 t ∧ Rlt t 2}.

Use reflexivity.

We prove the intermediate claim H0cond: Rlt 0 0 ∧ Rlt 0 2.

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt 0 t ∧ Rlt t 2) 0 H0open).

We prove the intermediate claim Hbad: Rlt 0 0.

An exact proof term for the current goal is (andEL (Rlt 0 0) (Rlt 0 2) H0cond).

An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hbad).

We prove the intermediate claim Hinj: ∀x y : set, x ∈ X → y ∈ X → apply_fun Fmap x = apply_fun Fmap y → x = y.

Let x and y be given.

Assume HxX: x ∈ X.

Assume HyX: y ∈ X.

Assume Heq: apply_fun Fmap x = apply_fun Fmap y.

Apply (xm (x = y)) to the current goal.

Assume Hxy: x = y.

An exact proof term for the current goal is Hxy.

Assume Hxyne: x ≠ y.

Set U to be the term X ∖ {y}.

We prove the intermediate claim HyCl: closed_in X Tx {y}.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) HT1 y HyX).

We prove the intermediate claim HUopen: U ∈ Tx.

We prove the intermediate claim HUin: open_in X Tx U.

An exact proof term for the current goal is (open_of_closed_complement X Tx {y} HyCl).

An exact proof term for the current goal is (open_in_elem X Tx U HUin).

We prove the intermediate claim HxU: x ∈ U.

Apply setminusI to the current goal.

An exact proof term for the current goal is HxX.

Assume HxY: x ∈ {y}.

We prove the intermediate claim Hxy: x = y.

An exact proof term for the current goal is (SingE y x HxY).

An exact proof term for the current goal is (Hxyne Hxy).

We prove the intermediate claim Hexh: ∃h : set, h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h ∧ apply_fun h x = 1 ∧ ∀z : set, z ∈ X ∖ U → apply_fun h z = 0.

An exact proof term for the current goal is (completely_regular_space_open_separator_unit_interval_in_function_space X Tx x U Hcr HxX HUopen HxU).

Apply Hexh to the current goal.

Let h be given.

Assume Hhpack: h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h ∧ apply_fun h x = 1 ∧ ∀z : set, z ∈ X ∖ U → apply_fun h z = 0.

We prove the intermediate claim Hhpair: (h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) ∧ apply_fun h x = 1.

An exact proof term for the current goal is (andEL ((h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) ∧ apply_fun h x = 1) (∀z : set, z ∈ X ∖ U → apply_fun h z = 0) Hhpack).

We prove the intermediate claim Hhzero: ∀z : set, z ∈ X ∖ U → apply_fun h z = 0.

An exact proof term for the current goal is (andER ((h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) ∧ apply_fun h x = 1) (∀z : set, z ∈ X ∖ U → apply_fun h z = 0) Hhpack).

We prove the intermediate claim Hhpair2: h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h.

An exact proof term for the current goal is (andEL (h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) (apply_fun h x = 1) Hhpair).

We prove the intermediate claim HhFS: h ∈ function_space X unit_interval.

An exact proof term for the current goal is (andEL (h ∈ function_space X unit_interval) (continuous_map X Tx unit_interval unit_interval_topology h) Hhpair2).

We prove the intermediate claim Hhcont: continuous_map X Tx unit_interval unit_interval_topology h.

An exact proof term for the current goal is (andER (h ∈ function_space X unit_interval) (continuous_map X Tx unit_interval unit_interval_topology h) Hhpair2).

We prove the intermediate claim Hhx1: apply_fun h x = 1.

An exact proof term for the current goal is (andER (h ∈ function_space X unit_interval ∧ continuous_map X Tx unit_interval unit_interval_topology h) (apply_fun h x = 1) Hhpair).

We prove the intermediate claim HhJ: h ∈ J.

An exact proof term for the current goal is (SepI (function_space X unit_interval) (λf0 : set ⇒ continuous_map X Tx unit_interval unit_interval_topology f0) h HhFS Hhcont).

Apply FalseE to the current goal.

We will prove False.

We prove the intermediate claim HyNotU: y ∉ U.

Assume HyU: y ∈ U.

We prove the intermediate claim HyNotSing: y ∉ {y}.

An exact proof term for the current goal is (setminusE2 X {y} y HyU).

An exact proof term for the current goal is (HyNotSing (SingI y)).

We prove the intermediate claim HyOut: y ∈ X ∖ U.

An exact proof term for the current goal is (setminusI X U y HyX HyNotU).

We prove the intermediate claim Hhy0: apply_fun h y = 0.

An exact proof term for the current goal is (Hhzero y HyOut).

We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x) h = apply_fun (apply_fun Fmap y) h.

rewrite the current goal using Heq (from left to right).

Use reflexivity.

We prove the intermediate claim HcoordEqx: apply_fun (apply_fun Fmap x) h = apply_fun h x.

rewrite the current goal using (diagonal_map_coord_apply X F J x h HxX HhJ) (from left to right).

We prove the intermediate claim HFdef: F = graph J (λf0 : set ⇒ f0).

Use reflexivity.

rewrite the current goal using HFdef (from left to right).

rewrite the current goal using (apply_fun_graph J (λf0 : set ⇒ f0) h HhJ) (from left to right).

Use reflexivity.

We prove the intermediate claim HcoordEqy: apply_fun (apply_fun Fmap y) h = apply_fun h y.

rewrite the current goal using (diagonal_map_coord_apply X F J y h HyX HhJ) (from left to right).

We prove the intermediate claim HFdef: F = graph J (λf0 : set ⇒ f0).

Use reflexivity.

rewrite the current goal using HFdef (from left to right).

rewrite the current goal using (apply_fun_graph J (λf0 : set ⇒ f0) h HhJ) (from left to right).

Use reflexivity.

We prove the intermediate claim HhEq: apply_fun h x = apply_fun h y.

rewrite the current goal using HcoordEqx (from right to left).

rewrite the current goal using HcoordEqy (from right to left).

An exact proof term for the current goal is HcoordEq.

We prove the intermediate claim H10: 1 = 0.

rewrite the current goal using Hhx1 (from right to left) at position 1.

rewrite the current goal using Hhy0 (from right to left).

An exact proof term for the current goal is HhEq.

We prove the intermediate claim Hpos01: Rlt 0 1.

An exact proof term for the current goal is (RltI 0 1 real_0 real_1 SNoLt_0_1).

We prove the intermediate claim Hbad: Rlt 0 0.

rewrite the current goal using H10 (from right to left) at position 2.

An exact proof term for the current goal is Hpos01.

An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) Hbad).

An exact proof term for the current goal is (embedding_of_from_local_refinement X Tx (unit_interval_power J) (product_topology_full J Xi) Fmap HcontFmap Hloc Hinj).