rcases M_LT'_N with ⟨X,Y,Z,claim⟩
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT'_N : ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N X Y Z : Multiset α
claim : Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLT M N