-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
rintro :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
rintro₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
refine_1 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    Z₂ + (Z₁ - Y₂) ≠ ∅
refine_2 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
refine_3 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
refine_4 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z) (y : α),
    y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
refine_2₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
refine_3₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
refine_4₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z) (y : α),
    y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
refine_3₂ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
refine_4₂ refine_4₃ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z) (y : α),
    y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
refine_4₄ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (∀ (x : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
      ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z
refine_4₅ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z) (y : α)
    (hy : y ∈ Y₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
refine_4₆ refine_4₇ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z) (y : α)
    (hy : y ∈ Y₂ - Z₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P

Tactic:
classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩

Premises used: Multiset.inter_add_sub_of_add_eq_add, add_assoc, or_imp, Multiset.mem_add, add_right_comm, add_left_inj, eq_comm, not_and_or, not_and, Multiset.inter_comm, rfl, forall_and