no goals
α : Type u_1
β : Type ?u.128187
γ : Type ?u.128190
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ diag {a} = {(a, a)}
rw [← product_sdiff_offDiag, offDiag_singleton, sdiff_empty, singleton_product_singleton]