ext b
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
⊢ M = X + {a0} - {a}
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
⊢ Multiset.count b M = Multiset.count b (X + {a0} - {a})