no goals
α : Type u_1
β : Type ?u.116188
γ : Type ?u.116191
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s ∪ offDiag s = s ×ˢ s
conv_rhs => rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]