Let n, x and y be given.
Assume Hx: x ∈ euclidean_space n.
Assume Hy: y ∈ euclidean_space n.
We prove the intermediate claim Hxy: (x,y) ∈ setprod (euclidean_space n) (euclidean_space n).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (euclidean_space n) (euclidean_space n) x y Hx Hy).
We prove the intermediate claim Hdef: euclidean_metric n = graph (setprod (euclidean_space n) (euclidean_space n)) (λp : set ⇒ Romega_D_metric_value (euclidean_space_extend_to_Romega n (p 0)) (euclidean_space_extend_to_Romega n (p 1))).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod (euclidean_space n) (euclidean_space n)) (λp : set ⇒ Romega_D_metric_value (euclidean_space_extend_to_Romega n (p 0)) (euclidean_space_extend_to_Romega n (p 1))) (x,y) Hxy) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
∎