rcases hLt with ⟨Z, X, y, a_def, b_def, X_lt_y⟩
case h.h.a.mp.base
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y a b : Multiset α
hLt : MultisetRedLt a b
⊢ MultisetLT a b
case h.h.a.mp.base.RedLt
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X✝ Y a b Z X : Multiset α
y : α
a_def : a = Z + X
b_def : b = Z + {y}
X_lt_y : ∀ y_1 ∈ X, y_1 < y
⊢ MultisetLT a b