have a0M: a0 ∈ M := by
  apply mul_mem_not_erase
  . change M = Multiset.erase (a0 ::ₘ X) a
    rw [mul_erase_trivial] at this0
    rw [mul_cons_trivial] at this0
    exact this0
  . exact hyp
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = M - {a0} + {a0}
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
a0M : a0 ∈ M
⊢ M = M - {a0} + {a0}