no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
m : Sym2 α
a : α
⊢ Finset.sym2 {a} = {Sym2.diag a}
rw [Finset.sym2, singleton_product_singleton, image_singleton, Sym2.diag, Quotient.mk']