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