-- 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 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⟩

Tactic:
specialize acc a _

Result:
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
⊢ a ∈ (↑⟨a :: l, hl⟩).head?

case mk.cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.Chain' (flip r) (a :: l)
acc : Acc r a
⊢ 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)
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
have hl' := (List.chain'_cons'.1 hl).2

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
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Proof state:
case mk.cons.intro.intro.h.mk.nil.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⟩
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) []
⊢ Acc (List.lex_chains r) ⟨[], hm⟩

Tactic:
apply Acc.intro

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

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:
apply Acc.intro

Result:
case mk.cons.intro.intro.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)
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨a :: ↑l, hl⟩ → Acc (List.lex_chains r) y

Proof state:
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
⊢ a ∈ (↑⟨a :: l, hl⟩).head?

Tactic:
rw [List.head?_cons, Option.mem_some_iff]

Result:
no goals

Proof state:
case mk.cons.intro.intro.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)
⊢ ∀ (y : List.chains r), List.lex_chains r y ⟨a :: ↑l, hl⟩ → Acc (List.lex_chains r) y

Tactic:
rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)

Result:
case mk.cons.intro.intro.h.mk.nil.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⟩
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) []
⊢ Acc (List.lex_chains r) ⟨[], hm⟩

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⟩

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⟩

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) 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⟩

Tactic:
clear_value l'

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
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩

Proof state:
α : 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'
⊢ l = ↑l'

Tactic:
rfl

Result:
no goals