rw [eq_comm] at hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a = a0
⊢ a0 ≠ a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : a ::ₘ M = X + {a0}
hyp : ¬a0 = a
⊢ a0 ≠ a