induction hLt with
| base a b hLt =>
  rcases hLt with ⟨Z, X, y, a_def, b_def, X_lt_y⟩
  use X
  simp
  simp
  assumption
| trans Z W A _ _ aih bih => exact LT_trans _ _ _ bih aih
case h.h.a.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
X Y : Multiset α
hLt : MultisetLt X Y
⊢ MultisetLT X Y
no goals