awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a : α
as m : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: as)
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) m
hmas : m ≤ as
nil : ∀ (hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) []) (hmas : [] ≤ as), IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]
cons :
  ∀ (b : α) (bs : List α) (hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)) (hmas : b :: bs ≤ as),
    IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: b :: bs)
⊢ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: m)

Tactic:
cases m with
  | nil => grind
  | cons b bs =>
    apply hm.cons_cons
    cases as with
    | nil =>
      simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
      exact (List.not_lt_nil _ hmas).elim
    | cons a' as =>
      rw [List.isChain_cons_cons] at ha
      refine lt_of_le_of_lt ?_ ha.1
      rw [le_iff_lt_or_eq] at hmas
      rcases hmas with hmas | hmas
      · exact head_le_of_lt hmas
      · simp_all only [List.cons.injEq, le_refl]

Premises used: reduceCtorEq, List.IsChain.cons_cons, le_refl, False.elim, List.not_lt_nil, List.IsChain.cons, List.cons.injEq, List.isChain_cons_cons, le_iff_lt_or_eq, List.IsChain.nil, or_false
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : IsChain R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
nil : ∀ (hl : IsChain R []) (hv : ∀ (lne : Ne.{u_1 + 1} (α := List α) [] []), R v (head [] lne)), IsChain R [v]
cons :
  ∀ (head : α) (tail : List α) (hl : IsChain R (head :: tail))
    (hv : ∀ (lne : head :: tail ≠ []), R v ((head :: tail).head lne)), IsChain R (v :: head :: tail)
⊢ IsChain R (v :: l)

Tactic:
cases l
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
R : α → α → Prop
v : α
hl : IsChain R []
hv : ∀ (lne : Ne.{u_1 + 1} (α := List α) [] []), R v (head [] lne)
⊢ IsChain R [v]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
R : α → α → Prop
v head : α
tail : List α
hl : IsChain R (head :: tail)
hv : ∀ (lne : head :: tail ≠ []), R v ((head :: tail).head lne)
⊢ IsChain R (v :: head :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
f : α → α
l : List α
hl : IsChain (fun (x y : α) ↦ f x = y) l
hi : 0 < l.length
⊢ f^[0] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 hi

Tactic:
rfl
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
f : α → α
l : List α
hl : IsChain (fun (x y : α) ↦ f x = y) l
i : ℕ
h :
  ∀ (hi : i < l.length),
    f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
hi : i + 1 < l.length
⊢ i < l.length

Tactic:
lia
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
f : α → α
l : List α
hl : IsChain (fun (x y : α) ↦ f x = y) l
i : ℕ
h :
  ∀ (hi : i < l.length),
    f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
hi : i + 1 < l.length
succ :
  f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi
⊢ f^[i + 1] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi

Tactic:
rw [Function.iterate_succ', Function.comp_apply, h (by lia)]

Premises used: Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
f : α → α
l : List α
hl : IsChain (fun (x y : α) ↦ f x = y) l
i : ℕ
h :
  ∀ (hi : i < l.length),
    f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
hi : i + 1 < l.length
succ :
  ∀
    (hl :
      ∀ (i : ℕ) (_hi : i + 1 < l.length),
        f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) =
          GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) _hi)
    (i : ℕ)
    (h :
      ∀ (hi : i < l.length),
        f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
          GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi)
    (hi : i + 1 < l.length),
    f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi
⊢ f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi

Tactic:
rw [List.isChain_iff_getElem] at hl

Premises used: List.isChain_iff_getElem
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
f : α → α
l : List α
hl :
  ∀ (i : ℕ) (_hi : i + 1 < l.length),
    f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) _hi
i : ℕ
h :
  ∀ (hi : i < l.length),
    f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
hi : i + 1 < l.length
⊢ f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi

Tactic:
apply hl
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
f : α → α
l : List α
hl : IsChain (fun (x y : α) ↦ f x = y) l
i : ℕ
hi : i < l.length
zero :
  ∀ (hi : 0 < l.length),
    f^[0] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 hi
succ :
  ∀ (i : ℕ)
    (h :
      ∀ (hi : i < l.length),
        f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
          GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi)
    (hi : i + 1 < l.length),
    f^[i + 1] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
      GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi
⊢ f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi

Tactic:
induction i with
  | zero => rfl
  | succ i h =>
    rw [Function.iterate_succ', Function.comp_apply, h (by lia)]
    rw [List.isChain_iff_getElem] at hl
    apply hl

Premises used: Function.iterate_succ', List.isChain_iff_getElem, Nat.zero, Function.comp_apply, Nat.succ
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
n : ℕ
a : α
h : r a a
zero : IsChain r (replicate 0 a)
one : IsChain r (replicate 1 a)
more : ∀ (n : ℕ), IsChain r (replicate n a) → IsChain r (replicate (n + 1) a) → IsChain r (replicate (n + 2) a)
⊢ IsChain r (replicate n a)

Tactic:
induction n using Nat.twoStepInduction
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 0 a)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a : α
h : r a a
⊢ IsChain r (replicate 1 a)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a : α
h : r a a
n : ℕ
h_1 : IsChain r (replicate n a)
h_2 : IsChain r (replicate (n + 1) a)
⊢ IsChain r (replicate (n + 2) a)

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) [] ↔
    ∀ (a : α), Membership.mem (γ := Option α) (head? []) a → [] = replicate (length.{u} (α := α) []) a

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
x : α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) [x] ↔ ∀ (a : α), a ∈ [x].head? → [x] = replicate [x].length a

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
a b : α
l : List α
IH : IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a
IH2 :
  ∀ (y : α),
    IsChain (fun (x1 x2 : α) ↦ x1 = x2) (y :: l) ↔ ∀ (a : α), a ∈ (y :: l).head? → y :: l = replicate (y :: l).length a
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) (a :: b :: l) ↔
    ∀ (a_1 : α), a_1 ∈ (a :: b :: l).head? → a :: b :: l = replicate (a :: b :: l).length a_1

Tactic:
simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

Premises used: eq_comm, List.isChain_cons_cons, List.replicate_succ
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
l : List α
nil :
  IsChain (fun (x1 x2 : α) ↦ x1 = x2) [] ↔
    ∀ (a : α), Membership.mem (γ := Option α) (head? []) a → [] = replicate (length.{u} (α := α) []) a
singleton : ∀ (x : α), IsChain (fun (x1 x2 : α) ↦ x1 = x2) [x] ↔ ∀ (a : α), a ∈ [x].head? → [x] = replicate [x].length a
cons_cons :
  ∀ (a b : α) (l : List α)
    (IH : IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a)
    (IH2 :
      ∀ (y : α),
        IsChain (fun (x1 x2 : α) ↦ x1 = x2) (y :: l) ↔
          ∀ (a : α), a ∈ (y :: l).head? → y :: l = replicate (y :: l).length a),
    IsChain (fun (x1 x2 : α) ↦ x1 = x2) (a :: b :: l) ↔
      ∀ (a_1 : α), a_1 ∈ (a :: b :: l).head? → a :: b :: l = replicate (a :: b :: l).length a_1
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a

Tactic:
induction l using twoStepInduction with
  | nil | singleton => simp
  | cons_cons a b l IH IH2 =>
    simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

Premises used: eq_comm, List.isChain_cons_cons, List.replicate_succ, Singleton.singleton, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
l : List α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a

Tactic:
induction l using twoStepInduction with
  | nil | singleton => simp
  | cons_cons a b l IH IH2 =>
    simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

Premises used: eq_comm, List.isChain_cons_cons, List.replicate_succ, Singleton.singleton, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
a : α
l : List α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) (a :: l) ↔ l = replicate l.length a

Tactic:
simp [isChain_eq_iff_eq_replicate, replicate_succ]

Premises used: List.replicate_succ, List.isChain_eq_iff_eq_replicate
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ (↑l : List α).head? → Acc r a
nil :
  ∀ (hl : List.IsChain (flip r) [])
    (acc :
      ∀ (a : α), a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl) : List α).head? → Acc r a),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl)
cons :
  ∀ (a : α) (l : List α) (hl : List.IsChain (flip r) (a :: l))
    (acc :
      ∀ (a_1 : α),
        a_1 ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head? → Acc r a_1),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
⊢ Acc (List.lex_chains r) l

Tactic:
obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
hl : List.IsChain (flip r) []
acc : ∀ (a : α), a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl) : List α).head? → Acc r a
nil :
  ∀ (y : List.chains r),
    List.lex_chains r y (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl) → Acc (List.lex_chains r) y
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl)

Tactic:
apply Acc.intro

Premises used: Acc.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc :
  ∀ (a_1 : α),
    a_1 ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head? → Acc r a_1
cons : a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head?
cons₁ :
  ∀ (acc : Acc r a), Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)

Tactic:
specialize acc a _
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc :
  ∀ (a_1 : α),
    a_1 ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head? → Acc r a_1
cons : a ∈ some a
cons₁ cons₂ : a = a
⊢ a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head?

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

Premises used: List.head?_cons, Option.mem_some_iff
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl : List.IsChain (flip r) (a :: l)
⊢ List.IsChain (flip r) l

Tactic:
have hl' := (List.isChain_cons.1 hl).2
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl : List.IsChain (flip r) (a :: l)
hl' : List.IsChain (flip r) l
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) l hl'
nil :
  ∀ (hl : List.IsChain (flip r) [a]) (hl' : List.IsChain (flip r) []),
    let l' := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl';
    Acc (List.lex_chains r) l'
cons :
  ∀ (b : α) (l : List α) (hl : List.IsChain (flip r) (a :: b :: l)) (hl' : List.IsChain (flip r) (b :: l)),
    let l' := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (b :: l) hl';
    Acc (List.lex_chains r) l'
⊢ Acc (List.lex_chains r) l'

Tactic:
rcases l with - | ⟨b, l⟩
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
hl : List.IsChain (flip r) [a]
hl' : List.IsChain (flip r) []
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl'
nil : ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y
⊢ Acc (List.lex_chains r) l'

Tactic:
apply Acc.intro

Premises used: Acc.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (b :: l) hl'
⊢ Acc (List.lex_chains r) l'

Tactic:
apply ih b (List.isChain_cons_cons.1 hl).1

Premises used: List.isChain_cons_cons, And.left, Iff.mp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl : List.IsChain (flip r) (a :: l)
hl' : List.IsChain (flip r) l
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) l hl'
⊢ Acc (List.lex_chains r) l'

Tactic:
have : Acc (List.lex_chains r) l' := by
      rcases l with - | ⟨b, l⟩
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      /- l' is accessible by induction hypothesis -/
      · apply ih b (List.isChain_cons_cons.1 hl).1
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl : List.IsChain (flip r) (a :: l)
hl' : List.IsChain (flip r) l
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) l hl'
this : Acc (List.lex_chains r) l'
cons :
  ∀ (hl : List.IsChain (flip r) (a :: l)),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)

Tactic:
revert hl
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) l hl'
this : Acc (List.lex_chains r) l'
⊢ l = (↑l' : List α)

Tactic:
rfl
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) l hl'
this : Acc (List.lex_chains r) l'
cons :
  ∀ (hl : List.IsChain (flip r) (a :: (↑l' : List α))),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l' : List α)) hl)
⊢ ∀ (hl : List.IsChain (flip r) (a :: l)),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)

Tactic:
rw [(by rfl : l = l'.1)]
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) l hl'
this : Acc (List.lex_chains r) l'
cons :
  ∀ (l' : List.chains r) (this : Acc (List.lex_chains r) l') (hl : List.IsChain (flip r) (a :: (↑l' : List α))),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l' : List α)) hl)
⊢ ∀ (hl : List.IsChain (flip r) (a :: (↑l' : List α))),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l' : List α)) hl)

Tactic:
clear_value l'
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l_1 : List α
hl' : List.IsChain (flip r) l_1
l' l : List.chains r
h_1 : ∀ (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.IsChain (flip r) (a :: (↑y : List α))),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑y : List α)) hl)
hl : List.IsChain (flip r) (a :: (↑l : List α))
cons :
  ∀ (y : List.chains r),
    List.lex_chains r y (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l : List α)) hl) →
      Acc (List.lex_chains r) y
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l : List α)) hl)

Tactic:
apply Acc.intro

Premises used: Acc.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l_1 : List α
hl' : List.IsChain (flip r) l_1
l' l : List.chains r
h_1 : ∀ (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.IsChain (flip r) (a :: (↑y : List α))),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑y : List α)) hl)
hl : List.IsChain (flip r) (a :: (↑l : List α))
hm : List.IsChain (flip r) []
cons :
  ∀ (y : List.chains r),
    List.lex_chains r y (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hm) → Acc (List.lex_chains r) y
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hm)

Tactic:
apply Acc.intro

Premises used: Acc.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l_1 : List α
hl' : List.IsChain (flip r) l_1
l' l : List.chains r
h_1 : ∀ (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.IsChain (flip r) (a :: (↑y : List α))),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑y : List α)) hl)
hl : List.IsChain (flip r) (a :: (↑l : List α))
b : α
m : List α
hm : List.IsChain (flip r) (b :: m)
hr : r b a
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (b :: m) hm)

Tactic:
apply ih b hr
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l_1 : List α
hl' : List.IsChain (flip r) l_1
l' l : List.chains r
h_1 : ∀ (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.IsChain (flip r) (a :: (↑y : List α))),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑y : List α)) hl)
hl : List.IsChain (flip r) (a :: (↑l : List α))
m : List α
hm : List.IsChain (flip r) (a :: m)
hr : List.Lex r m (↑l : List α)
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: m) hm)

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

Premises used: Subtype.mk, And.right, List.isChain_cons, Iff.mp