-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma transGen_oneStep_of_isDershowitzMannaLT :
    IsDershowitzMannaLT M N → TransGen OneStep M N

Proof state:
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ y ∈ Y, ∃ z ∈ 0, y < z) → TransGen Multiset.OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ 0, y < z_1
⊢ ∀ y ∈ Y, y < z

Tactic:
simpa using hYZ

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.cons
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
⊢ TransGen Multiset.OneStep M N

Tactic:
obtain rfl | hZ := eq_or_ne Z 0

Result:
case intro.intro.intro.intro.intro.intro.cons.inl
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ y ∈ Y, ∃ z ∈ 0, y < z) → TransGen Multiset.OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ 0, y < z_1
⊢ TransGen Multiset.OneStep M N

case intro.intro.intro.intro.intro.intro.cons.inr
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
⊢ TransGen Multiset.OneStep M N

Proof state:
case intro.intro.intro.intro.intro.intro.cons.inr.refine_1
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
⊢ M = X + Y' + (Y - Y')

Tactic:
rw [add_add_tsub_cancel (filter_le ..), hM]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.cons.inl
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ y ∈ Y, ∃ z ∈ 0, y < z) → TransGen Multiset.OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ 0, y < z_1
⊢ TransGen Multiset.OneStep M N

Tactic:
exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
⊢ N = X + Z + {z}

Tactic:
simp [hN, add_comm (_ + _)]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M N X Y Z : Multiset α
hZ : Z ≠ ∅
hM : M = X + Y
hN : N = X + Z
hYZ : ∀ y ∈ Y, ∃ z ∈ Z, y < z
⊢ TransGen Multiset.OneStep M N

Tactic:
induction' Z using Multiset.induction_on with z Z ih generalizing X Y M N

Result:
case intro.intro.intro.intro.intro.intro.empty
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
hZ : 0 ≠ ∅
hM : M = X + Y
hN : N = X + 0
hYZ : ∀ y ∈ Y, ∃ z ∈ 0, y < z
⊢ TransGen Multiset.OneStep M N

case intro.intro.intro.intro.intro.intro.cons
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
⊢ TransGen Multiset.OneStep M N

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

Tactic:
rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M N X Y Z : Multiset α
hZ : Z ≠ ∅
hM : M = X + Y
hN : N = X + Z
hYZ : ∀ y ∈ Y, ∃ z ∈ Z, y < z
⊢ TransGen Multiset.OneStep M N

Proof state:
case intro.intro.intro.intro.intro.intro.cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z ∈ Z, y < z

Tactic:
simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy

Result:
case intro.intro.intro.intro.intro.intro.cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ ∃ z ∈ Z, y < z

Proof state:
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
⊢ ∀ y ∈ Y', y < z

Tactic:
simp [Y']

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.empty
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
hZ : 0 ≠ ∅
hM : M = X + Y
hN : N = X + 0
hYZ : ∀ y ∈ Y, ∃ z ∈ 0, y < z
⊢ TransGen Multiset.OneStep M N

Tactic:
simp at hZ

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ y ∈ Y

Tactic:
aesop

Result:
no goals