no goals
α : Type u_1
β : Type ?u.128864
γ : Type ?u.128867
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a : α
⊢ diag (insert a s) = insert (a, a) (diag s)
rw [insert_eq, insert_eq, diag_union, diag_singleton]