-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
rintro :
  ∀ (X Y Z : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
cons :
  ∀ (z : α) (Z : Multiset α)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
        (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N)
    {M N : Multiset α} (X Y : Multiset α) (hZ : z ::ₘ Z ≠ ∅) (hM : M = X + Y) (hN : N = X + z ::ₘ Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1), TransGen OneStep M N
cons₁ :
  ∀ (z : α) {M N : Multiset α} (X Y : Multiset α) (hM : M = X + Y)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Ne.{u_1 + 1} (α := Multiset α) 0 ∅) (hM : M = X + Y)
        (hN : N = X + 0) (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) 0 z ∧ y < z),
        TransGen OneStep M N)
    (hZ : z ::ₘ 0 ≠ ∅) (hN : N = X + z ::ₘ 0) (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ 0 ∧ y < z_1),
    TransGen OneStep M N
cons₂ cons₃ :
  ∀ (z : α) (Z : Multiset α)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
        (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N)
    {M N : Multiset α} (X Y : Multiset α) (hZ : z ::ₘ Z ≠ ∅) (hM : M = X + Y) (hN : N = X + z ::ₘ Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1) (hZ : Z ≠ 0), TransGen OneStep M N
cons₄ :
  ∀ (z : α) (Z : Multiset α)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
        (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N)
    {M N : Multiset α} (X Y : Multiset α) (hZ : z ::ₘ Z ≠ ∅) (hM : M = X + Y) (hN : N = X + z ::ₘ Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1) (hZ : Z ≠ 0), TransGen OneStep M N
cons₅ :
  ∀ (z : α) (Z : Multiset α)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
        (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N)
    {M N : Multiset α} (X Y : Multiset α) (hZ : z ::ₘ Z ≠ ∅) (hM : M = X + Y) (hN : N = X + z ::ₘ Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1) (hZ : Z ≠ 0),
    let Y' := filter (fun (x : α) ↦ x < z) Y;
    M = X + Y' + (Y - Y')
cons₆ cons₇ :
  ∀ (z : α) (Z : Multiset α)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
        (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N)
    {M N : Multiset α} (X Y : Multiset α) (hZ : z ::ₘ Z ≠ ∅) (hM : M = X + Y) (hN : N = X + z ::ₘ Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1) (hZ : Z ≠ 0),
    let Y' := filter (fun (x : α) ↦ x < z) Y;
    ∀ (y : α) (hy : y ∈ Y - Y'), ∃ (z : α), z ∈ Z ∧ y < z
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N

Tactic:
classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  refine .tail (b := X + Y' + Z) (ih (X + Y') (Y - Y') hZ ?_ rfl fun y hy ↦ ?_) <|
    ⟨X + Z, Y', z, add_right_comm .., by simp [hN, add_comm (_ + _)], by simp [Y']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)

Premises used: Multiset.cons, add_add_tsub_cancel, Multiset.filter_le, Multiset.mem_filter, Multiset.sub_filter_eq_filter_not, rfl