no goals
α : Type u_1
β : Type ?u.445536
γ : Type ?u.445539
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ toFinset {a} = {a}
rw [← cons_zero, toFinset_cons, toFinset_zero, IsLawfulSingleton.insert_emptyc_eq]