simp_all
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
ba0 : ¬b = a0
this : Multiset.count b M = Multiset.count b (a ::ₘ M)
⊢ Multiset.count b X + Multiset.count b {a0} = Multiset.count b ((a0 ::ₘ X).erase a)
no goals