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