simp [mul_cons_trivial, mul_erase_trivial] at *
α : 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 α
hyp : a = a0
H : a ::ₘ M = a0 ::ₘ X
⊢ M = (a0 ::ₘ X).erase a