rw [ba0]
α : 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
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
α : 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
⊢ Multiset.count a0 M = (Multiset.count a0 X + if a0 = a0 then 1 else 0) - if a0 = a then 1 else 0