no goals
α : Type u_1
β : Type ?u.365585
γ : Type ?u.365588
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) a) = count a (Quotient.mk (isSetoid α) l) - 1
convert List.count_erase_self a l <;> rw [←coe_count] <;> simp