rw [H1]
case h.left
α : 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
⊢ N = M + Y
case h.left
α : 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
⊢ X + Y = M + Y