no goals
α : Type u_1
β : Type ?u.120722
γ : Type ?u.120725
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ s ×ˢ s \ offDiag s = diag s
rw [← diag_union_offDiag, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _)]