no goals
α : Type u_1
β : Type ?u.376488
γ : Type ?u.376491
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) b) = count a (Quotient.mk (isSetoid α) l)
convert List.count_erase_of_ne ab l <;> rw [←coe_count] <;> simp