-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma acc_oneStep_cons_of_acc_lt (ha : Acc LT.lt a) :
    ∀ {M}, Acc OneStep M → Acc OneStep (a ::ₘ M)

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
⊢ ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (a ::ₘ M)

Tactic:
rintro M hM

Result:
case intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M : Multiset α
hM : Acc Multiset.OneStep M
⊢ Acc Multiset.OneStep (a ::ₘ M)

Proof state:
case intro.intro.intro.inr.intro.empty
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
hN : ∀ x ∈ 0, x < a
⊢ Acc Multiset.OneStep (M + 0)

Tactic:
simpa using .intro _ hM

Result:
no goals

Proof state:
case intro.intro.intro.inr.intro.cons
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ x ∈ N, x < a) → Acc Multiset.OneStep (M + N)
hN : b < a ∧ ∀ a_1 ∈ N, a_1 < a
⊢ Acc Multiset.OneStep (b ::ₘ (M + N))

Tactic:
obtain ⟨hba, hN⟩ := hN

Result:
case intro.intro.intro.inr.intro.cons.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ x ∈ N, x < a) → Acc Multiset.OneStep (M + N)
hba : b < a
hN : ∀ a_1 ∈ N, a_1 < a
⊢ Acc Multiset.OneStep (b ::ₘ (M + N))

Proof state:
case intro.intro.intro.inr.intro.cons
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ x ∈ N, x < a) → Acc Multiset.OneStep (M + N)
hN : ∀ x ∈ b ::ₘ N, x < a
⊢ Acc Multiset.OneStep (M + b ::ₘ N)

Tactic:
simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢

Result:
case intro.intro.intro.inr.intro.cons
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ x ∈ N, x < a) → Acc Multiset.OneStep (M + N)
hN : b < a ∧ ∀ a_1 ∈ N, a_1 < a
⊢ Acc Multiset.OneStep (b ::ₘ (M + N))

Proof state:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
⊢ Acc Multiset.OneStep (a ::ₘ M)

Tactic:
refine .intro _ fun N hNM ↦ ?_

Result:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hNM : Multiset.OneStep N (a ::ₘ M)
⊢ Acc Multiset.OneStep N

Proof state:
case intro.intro.intro.inr.intro.cons.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : (∀ x ∈ N, x < a) → Acc Multiset.OneStep (M + N)
hba : b < a
hN : ∀ a_1 ∈ N, a_1 < a
⊢ Acc Multiset.OneStep (b ::ₘ (M + N))

Tactic:
exact ha _ hba <| ihN hN

Result:
no goals

Proof state:
case intro.intro.intro.inl.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hNM' : Multiset.OneStep N M
hNM : Multiset.OneStep (a ::ₘ N) (a ::ₘ M)
⊢ Acc Multiset.OneStep (a ::ₘ N)

Tactic:
exact ihM _ hNM'

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hNM : Multiset.OneStep N (a ::ₘ M)
⊢ Acc Multiset.OneStep N

Tactic:
obtain ⟨N, ⟨rfl, hNM'⟩ | ⟨rfl, hN⟩⟩ := isDershowitzMannaLT_singleton_insert hNM

Result:
case intro.intro.intro.inl.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hNM' : Multiset.OneStep N M
hNM : Multiset.OneStep (a ::ₘ N) (a ::ₘ M)
⊢ Acc Multiset.OneStep (a ::ₘ N)

case intro.intro.intro.inr.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ x ∈ N, x < a
hNM : Multiset.OneStep (M + N) (a ::ₘ M)
⊢ Acc Multiset.OneStep (M + N)

Proof state:
case intro.intro.intro.inr.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ x ∈ N, x < a
hNM : Multiset.OneStep (M + N) (a ::ₘ M)
⊢ Acc Multiset.OneStep (M + N)

Tactic:
clear hNM

Result:
case intro.intro.intro.inr.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ y < a, Acc LT.lt y
ha : ∀ y < a, ∀ {M : Multiset α}, Acc Multiset.OneStep M → Acc Multiset.OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep y
ihM : ∀ (y : Multiset α), Multiset.OneStep y M → Acc Multiset.OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ x ∈ N, x < a
⊢ Acc Multiset.OneStep (M + N)