Let J, x and y be given.
Assume Hx: x ∈ power_real J.
Assume Hy: y ∈ power_real J.
We prove the intermediate claim Hxy: (x,y) ∈ setprod (power_real J) (power_real J).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (power_real J) (power_real J) x y Hx Hy).
We prove the intermediate claim Hddef: uniform_metric_power_real J = graph (setprod (power_real J) (power_real J)) (λp : set ⇒ power_real_uniform_metric_value J (p 0) (p 1)).
Use reflexivity.
rewrite the current goal using Hddef (from left to right).
rewrite the current goal using (apply_fun_graph (setprod (power_real J) (power_real J)) (λp : set ⇒ power_real_uniform_metric_value J (p 0) (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.
∎