apply MultisetLT.MLT X Y Z
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
case mpr.intro.intro.intro.a
α : 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
⊢ Y ≠ ∅

case mpr.intro.intro.intro.a
α : 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
⊢ M = Z + X

case mpr.intro.intro.intro.a
α : 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
⊢ N = Z + Y

case mpr.intro.intro.intro.a
α : 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
⊢ ∀ x ∈ X, ∃ y ∈ Y, x < y