simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M + {a}) = Multiset.count a✝ (a ::ₘ M)
no goals