-- 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.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₂) ≠ ∅

Tactic:
simpa [-not_and, not_and_or] using .inl hZ₂

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4.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
y : α
hy : y ∈ Y₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4.refine_1.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, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Proof state:
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

Tactic:
exact ⟨z, .inl hz, hyz⟩

Result:
no goals

Proof state:
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

Tactic:
simp only [mem_add, or_imp, forall_and]

Result:
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
⊢ (∀ x ∈ Y₁, ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧ ∀ x ∈ Y₂ - Z₁, ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z

Proof state:
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₂))

Tactic:
rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]

Result:
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
⊢ Y₂ + X₂ = Z₁ + X₁

Proof state:
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
⊢ (∀ x ∈ Y₁, ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧ ∀ x ∈ Y₂ - Z₁, ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z

Tactic:
refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4.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
y : α
hy : y ∈ Y₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

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

Proof state:
α : 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₁ - Y₂

Tactic:
rwa [mem_sub, count_eq_zero_of_not_mem z_in, count_pos]

Result:
no goals

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 : X₁ + Z₁ = X₂ + Y₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Tactic:
rw [add_comm X₁,add_comm X₂] at hXZXY

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 : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ y ∈ Y₂, ∃ z ∈ Z₂, y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Proof state:
case pos
α : 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:
obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in

Result:
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

Proof state:
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
⊢ Y₂ + X₂ = Z₁ + X₁

Tactic:
rwa [eq_comm]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_4.refine_1.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, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
by_cases z_in : z ∈ Y₂

Result:
case pos
α : 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

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