ext
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
⊢ M - {a} = M.erase a
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M - {a}) = Multiset.count a✝ (M.erase a)