no goals
α : Type u_1
β : Type ?u.129768
γ : Type ?u.129771
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
has : ¬a ∈ s
⊢ offDiag (insert a s) = offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}
rw [insert_eq, union_comm, offDiag_union (disjoint_singleton_right.2 has), offDiag_singleton,
  union_empty, union_right_comm]