Let X, d, A, x and y be given.

Assume HxA: x ∈ A.

Assume HyA: y ∈ A.

We prove the intermediate claim Hxy: (x,y) ∈ setprod A A.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma A A x y HxA HyA).

rewrite the current goal using (metric_restrict_def X d A) (from left to right) at position 1.

rewrite the current goal using (apply_fun_graph (setprod A A) (λp : set ⇒ apply_fun d p) (x,y) Hxy) (from left to right).

Use reflexivity.

∎