-- Mathlib/Data/Multiset/DershowitzManna.lean
/-- `IsDershowitzMannaLT` is transitive. -/
lemma IsDershowitzMannaLT.trans :
    IsDershowitzMannaLT M N → IsDershowitzMannaLT N P → IsDershowitzMannaLT M P

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Tactic:
refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ Z₂ + (Z₁ - Y₂) ≠ ∅

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ ∀ y ∈ Y₁ + (Y₂ - Z₁), ∃ z ∈ Z₂ + (Z₁ - Y₂), y < z

Proof state:
case neg
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∉ Y₂
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_not_mem z_in, count_pos], hyz⟩

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
w : α
hw : w ∈ Z₂
hzw : z < w
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨w, .inl hw, hyz.trans hzw⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

Tactic:
rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
M N P : Multiset α
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P

Tactic:
rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : X₁ + Z₁ = X₂ + Y₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
y : α
hy : y ∈ Y₂ - Z₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4.refine_2.intro.intro
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ y ∈ Y₁, ∃ z ∈ Z₁, y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
y : α
hy : y ∈ Y₂ - Z₁
z : α
hz : z ∈ Z₂
hyz : y < z
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z