Let X, F, J, x and i be given.
Assume HxX: x ∈ X.
Assume HiJ: i ∈ J.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
rewrite the current goal using HdiagDef (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX) (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
∎