-- Mathlib/Data/List/Chain.lean
theorem Acc.list_chain' {l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r a) :
    Acc (List.lex_chains r) l

Proof state:
case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.Chain' (flip r) [a]
hl' : List.Chain' (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
apply Acc.intro

Result:
case nil.h
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.Chain' (flip r) [a]
hl' : List.Chain' (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y

Proof state:
case nil.h
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.Chain' (flip r) [a]
hl' : List.Chain' (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y

Tactic:
rintro ⟨_⟩ ⟨_⟩

Result:
no goals

Proof state:
case mk.nil.h
α : Type u_1
r : α → α → Prop
hl : List.Chain' (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hl⟩ → Acc (List.lex_chains r) y

Tactic:
rintro ⟨_⟩ ⟨_⟩

Result:
no goals

Proof state:
case mk.cons.intro.intro.h.mk.cons.cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.Chain' (flip r) (a :: ↑l)
m : List α
hm : List.Chain' (flip r) (a :: m)
hr : List.Lex r m ↑l
⊢ Acc (List.lex_chains r) ⟨a :: m, hm⟩

Tactic:
apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.Chain' (flip r) (a :: b :: l)
hl' : List.Chain' (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
apply ih b (List.chain'_cons.1 hl).1

Result:
no goals

Proof state:
case mk.cons.intro.intro.h.mk.nil.nil.h
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.Chain' (flip r) (a :: ↑l)
hm : List.Chain' (flip r) []
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hm⟩ → Acc (List.lex_chains r) y

Tactic:
rintro ⟨_⟩ ⟨_⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a
⊢ Acc (List.lex_chains r) l

Tactic:
obtain ⟨_ | ⟨a, l⟩, hl⟩ := l

Result:
case mk.nil
α : Type u_1
r : α → α → Prop
hl : List.Chain' (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩

case mk.cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.Chain' (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Proof state:
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
let l' : List.chains r := ⟨l, hl'⟩

Result:
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
l' : List.chains r := ⟨l, hl'⟩
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Proof state:
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
revert hl

Result:
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: l)), Acc (List.lex_chains r) ⟨a :: l, hl⟩

Proof state:
case mk.cons.intro.intro.h.mk.cons.rel
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.Chain' (flip r) (a :: ↑l)
b : α
m : List α
hm : List.Chain' (flip r) (b :: m)
hr : r b a
⊢ Acc (List.lex_chains r) ⟨b :: m, hm⟩

Tactic:
apply ih b hr

Result:
no goals

Proof state:
case mk.cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l)), Acc (List.lex_chains r) ⟨a :: ↑l, hl⟩

Tactic:
intro hl

Result:
case mk.cons.intro.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.Chain' (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.Chain' (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.Chain' (flip r) (a :: ↑l)
⊢ Acc (List.lex_chains r) ⟨a :: ↑l, hl⟩

Proof state:
case mk.nil
α : Type u_1
r : α → α → Prop
hl : List.Chain' (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ Acc (List.lex_chains r) ⟨[], hl⟩

Tactic:
apply Acc.intro

Result:
case mk.nil.h
α : Type u_1
r : α → α → Prop
hl : List.Chain' (flip r) []
acc : ∀ (a : α), a ∈ (↑⟨[], hl⟩).head? → Acc r a
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨[], hl⟩ → Acc (List.lex_chains r) y