Let p be given.

Assume Hp: p ∈ setprod X X.

We will prove apply_fun d p ∈ R.

We prove the intermediate claim Hp0: p 0 ∈ X.

An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ X) p Hp).

We prove the intermediate claim Hp1: p 1 ∈ X.

An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ X) p Hp).

We prove the intermediate claim Hval: apply_fun d p = Romega_D_metric_value (euclidean_space_extend_to_Romega n (p 0)) (euclidean_space_extend_to_Romega n (p 1)).

We prove the intermediate claim Hdef: d = graph (setprod X X) (λq : set ⇒ Romega_D_metric_value (euclidean_space_extend_to_Romega n (q 0)) (euclidean_space_extend_to_Romega n (q 1))).

Use reflexivity.

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

An exact proof term for the current goal is (apply_fun_graph (setprod X X) (λq : set ⇒ Romega_D_metric_value (euclidean_space_extend_to_Romega n (q 0)) (euclidean_space_extend_to_Romega n (q 1))) p Hp).

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

We prove the intermediate claim Hx0: euclidean_space_extend_to_Romega n (p 0) ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n (p 0) Hp0).

We prove the intermediate claim Hx1: euclidean_space_extend_to_Romega n (p 1) ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n (p 1) Hp1).

An exact proof term for the current goal is (Romega_D_metric_value_in_R (euclidean_space_extend_to_Romega n (p 0)) (euclidean_space_extend_to_Romega n (p 1)) Hx0 Hx1).

Let x and y be given.

Assume Hx: x ∈ X.

Assume Hy: y ∈ X.

We will prove apply_fun d (x,y) = apply_fun d (y,x).

We prove the intermediate claim Hxy: apply_fun d (x,y) = Romega_D_metric_value (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y).

An exact proof term for the current goal is (euclidean_metric_apply n x y Hx Hy).

We prove the intermediate claim Hyx: apply_fun d (y,x) = Romega_D_metric_value (euclidean_space_extend_to_Romega n y) (euclidean_space_extend_to_Romega n x).

An exact proof term for the current goal is (euclidean_metric_apply n y x Hy Hx).

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

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

We prove the intermediate claim Hextx: euclidean_space_extend_to_Romega n x ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n x Hx).

We prove the intermediate claim Hexty: euclidean_space_extend_to_Romega n y ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n y Hy).

An exact proof term for the current goal is (Romega_D_metric_value_sym (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) Hextx Hexty).

Let x be given.

Assume Hx: x ∈ X.

We will prove apply_fun d (x,x) = 0.

We prove the intermediate claim Hxx: apply_fun d (x,x) = Romega_D_metric_value (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n x).

An exact proof term for the current goal is (euclidean_metric_apply n x x Hx Hx).

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

We prove the intermediate claim Hextx: euclidean_space_extend_to_Romega n x ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n x Hx).

An exact proof term for the current goal is (Romega_D_metric_value_self_zero (euclidean_space_extend_to_Romega n x) Hextx).

Let x and y be given.

Assume Hx: x ∈ X.

Assume Hy: y ∈ X.

We will prove ¬ (Rlt (apply_fun d (x,y)) 0) ∧ (apply_fun d (x,y) = 0 → x = y).

Apply andI to the current goal.

We prove the intermediate claim HmD: metric_on R_omega_space Romega_D_metric.

An exact proof term for the current goal is (andEL (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).

We prove the intermediate claim Hextx: euclidean_space_extend_to_Romega n x ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n x Hx).

We prove the intermediate claim Hexty: euclidean_space_extend_to_Romega n y ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n y Hy).

We prove the intermediate claim Hdxy: apply_fun d (x,y) = apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y).

We prove the intermediate claim Hxyprod: (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) ∈ setprod R_omega_space R_omega_space.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) Hextx Hexty).

We prove the intermediate claim HappD: apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) = Romega_D_metric_value (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y).

We prove the intermediate claim HdefD: Romega_D_metric = graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)).

Use reflexivity.

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

rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) Hxyprod) (from left to right).

rewrite the current goal using (tuple_2_0_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y)) (from left to right).

rewrite the current goal using (tuple_2_1_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y)) (from left to right).

Use reflexivity.

rewrite the current goal using (euclidean_metric_apply n x y Hx Hy) (from left to right).

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

Use reflexivity.

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

An exact proof term for the current goal is (metric_on_nonneg R_omega_space Romega_D_metric (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) HmD Hextx Hexty).

Assume H0: apply_fun d (x,y) = 0.

We prove the intermediate claim HmD: metric_on R_omega_space Romega_D_metric.

An exact proof term for the current goal is (andEL (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).

We prove the intermediate claim Hextx: euclidean_space_extend_to_Romega n x ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n x Hx).

We prove the intermediate claim Hexty: euclidean_space_extend_to_Romega n y ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n y Hy).

We prove the intermediate claim Hdxy: apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) = 0.

We prove the intermediate claim Hxyprod: (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) ∈ setprod R_omega_space R_omega_space.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) Hextx Hexty).

We prove the intermediate claim HdefD: Romega_D_metric = graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)).

Use reflexivity.

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

rewrite the current goal using (tuple_2_0_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y)) (from left to right).

rewrite the current goal using (tuple_2_1_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y)) (from left to right).

Use reflexivity.

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

rewrite the current goal using (euclidean_metric_apply n x y Hx Hy) (from right to left) at position 1.

An exact proof term for the current goal is H0.

We prove the intermediate claim HextEq: euclidean_space_extend_to_Romega n x = euclidean_space_extend_to_Romega n y.

An exact proof term for the current goal is (metric_on_zero_eq R_omega_space Romega_D_metric (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) HmD Hextx Hexty Hdxy).

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_injective n x y HnO Hx Hy HextEq).

Let x, y and z be given.

Assume Hx: x ∈ X.

Assume Hy: y ∈ X.

Assume Hz: z ∈ X.

We prove the intermediate claim HmD: metric_on R_omega_space Romega_D_metric.

An exact proof term for the current goal is (andEL (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).

We prove the intermediate claim Hextx: euclidean_space_extend_to_Romega n x ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n x Hx).

We prove the intermediate claim Hexty: euclidean_space_extend_to_Romega n y ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n y Hy).

We prove the intermediate claim Hextz: euclidean_space_extend_to_Romega n z ∈ R_omega_space.

An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space n z Hz).

We prove the intermediate claim HtriD: ¬ (Rlt (add_SNo (apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y)) (apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n y,euclidean_space_extend_to_Romega n z))) (apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n z))).

An exact proof term for the current goal is (metric_on_triangle R_omega_space Romega_D_metric (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) (euclidean_space_extend_to_Romega n z) HmD Hextx Hexty Hextz).

We prove the intermediate claim Hxyprod: (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) ∈ setprod R_omega_space R_omega_space.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y) Hextx Hexty).

We prove the intermediate claim Hyzprod: (euclidean_space_extend_to_Romega n y,euclidean_space_extend_to_Romega n z) ∈ setprod R_omega_space R_omega_space.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space (euclidean_space_extend_to_Romega n y) (euclidean_space_extend_to_Romega n z) Hexty Hextz).

We prove the intermediate claim Hxzprod: (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n z) ∈ setprod R_omega_space R_omega_space.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n z) Hextx Hextz).

We prove the intermediate claim Happxy: apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n y) = Romega_D_metric_value (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y).

We prove the intermediate claim HdefD: Romega_D_metric = graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)).

Use reflexivity.

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

rewrite the current goal using (tuple_2_0_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y)) (from left to right).

rewrite the current goal using (tuple_2_1_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n y)) (from left to right).

Use reflexivity.

We prove the intermediate claim Happyz: apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n y,euclidean_space_extend_to_Romega n z) = Romega_D_metric_value (euclidean_space_extend_to_Romega n y) (euclidean_space_extend_to_Romega n z).

We prove the intermediate claim HdefD: Romega_D_metric = graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)).

Use reflexivity.

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

rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (euclidean_space_extend_to_Romega n y,euclidean_space_extend_to_Romega n z) Hyzprod) (from left to right).

rewrite the current goal using (tuple_2_0_eq (euclidean_space_extend_to_Romega n y) (euclidean_space_extend_to_Romega n z)) (from left to right).

rewrite the current goal using (tuple_2_1_eq (euclidean_space_extend_to_Romega n y) (euclidean_space_extend_to_Romega n z)) (from left to right).

Use reflexivity.

We prove the intermediate claim Happxz: apply_fun Romega_D_metric (euclidean_space_extend_to_Romega n x,euclidean_space_extend_to_Romega n z) = Romega_D_metric_value (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n z).

We prove the intermediate claim HdefD: Romega_D_metric = graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)).

Use reflexivity.

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

rewrite the current goal using (tuple_2_0_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n z)) (from left to right).

rewrite the current goal using (tuple_2_1_eq (euclidean_space_extend_to_Romega n x) (euclidean_space_extend_to_Romega n z)) (from left to right).

Use reflexivity.

rewrite the current goal using (euclidean_metric_apply n x y Hx Hy) (from left to right) at position 1.

rewrite the current goal using (euclidean_metric_apply n y z Hy Hz) (from left to right) at position 1.

rewrite the current goal using (euclidean_metric_apply n x z Hx Hz) (from left to right) at position 1.

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

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

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

An exact proof term for the current goal is HtriD.