have a0_a: a0 ≠ a := by rw [eq_comm] at hyp; exact hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
⊢ M = X + {a0} - {a}
α : 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}