awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as ∨ b :: bs = a' :: as
⊢ b ≤ a'
have cons : ∀ (hmas : b :: bs < a' :: as), b ≤ a'
Tactic: rcases hmas with hmas | hmas
Cleared hypotheses: hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as ∨ b :: bs = a' :: as
cons : ∀ (hmas : b :: bs < a' :: as), b ≤ a'
⊢ b ≤ a'
have cons₁ : ∀ (hmas : b :: bs = a' :: as), b ≤ a'
Tactic: rcases hmas with hmas | hmas
Cleared hypotheses: hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
inst : LinearOrder α
a : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ a > b
have cons : ∀ (ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]) (hmas : b :: bs ≤ []), a > b
Tactic: 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]
Cleared hypotheses: as, ha, hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
inst : LinearOrder α
a : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
cons : ∀ (ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]) (hmas : b :: bs ≤ []), a > b
⊢ a > b
have cons₁ : ∀ (a' : α) (as : List α) (ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: a' :: as)) (hmas : b :: bs ≤ a' :: as), a > b
Tactic: 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]
Cleared hypotheses: as, ha, hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: m)
have nil : ∀ (hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) []) (hmas : [] ≤ as), IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]
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]
Cleared hypotheses: m, hm, hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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]
⊢ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: m)
have 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)
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]
Cleared hypotheses: m, hm, hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u_1
R : α → α → Prop
l : List α
v : α
hl : IsChain R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ IsChain R (v :: l)
have nil : ∀ (hl : IsChain R []) (hv : ∀ (lne : Ne.{u_1 + 1} (α := List α) [] []), R v (head [] lne)), IsChain R [v]
Tactic: cases l
Cleared hypotheses: l, hl, hv
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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]
⊢ IsChain R (v :: l)
have cons : ∀ (head : α) (tail : List α) (hl : IsChain R (head :: tail))
  (hv : ∀ (lne : head :: tail ≠ []), R v ((head :: tail).head lne)), IsChain R (v :: head :: tail)
Tactic: cases l
Cleared hypotheses: l, hl, hv
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ 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
have succ : f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry) =
  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)]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ 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
have succ : ∀
  (hl :
    ∀ (i : ℕ) (_hi : i + 1 < l.length),
      f (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry) =
        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 sorry) =
        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 sorry) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) hi
Tactic: rw [List.isChain_iff_getElem] at hl
Cleared hypotheses: hl, i, h, hi
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u_1
f : α → α
l : List α
hl : IsChain (fun (x y : α) ↦ f x = y) l
i : ℕ
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
have zero : ∀ (hi : 0 < l.length),
  f^[0] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 sorry) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 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
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ 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
have succ : ∀ (i : ℕ)
  (h :
    ∀ (hi : i < l.length),
      f^[i] (GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 sorry) =
        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 sorry) =
    GetElem.getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + 1) 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
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
n : ℕ
a : α
h : r a a
⊢ IsChain r (replicate n a)
have zero : IsChain r (replicate 0 a)
Tactic: induction n using Nat.twoStepInduction
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
n : ℕ
a : α
h : r a a
zero : IsChain r (replicate 0 a)
⊢ IsChain r (replicate n a)
have one : IsChain r (replicate 1 a)
Tactic: induction n using Nat.twoStepInduction
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
n : ℕ
a : α
h : r a a
zero : IsChain r (replicate 0 a)
one : IsChain r (replicate 1 a)
⊢ IsChain r (replicate n a)
have more : ∀ (n : ℕ), IsChain r (replicate n a) → IsChain r (replicate (n + 1) a) → IsChain r (replicate (n + 2) a)
Tactic: induction n using Nat.twoStepInduction
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
l : List α
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a
have nil : IsChain (fun (x1 x2 : α) ↦ x1 = x2) [] ↔
  ∀ (a : α), Membership.mem (γ := Option α) (head? []) a → [] = replicate (length.{u} (α := α) []) 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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
l : List α
nil :
  IsChain (fun (x1 x2 : α) ↦ x1 = x2) [] ↔
    ∀ (a : α), Membership.mem (γ := Option α) (head? []) a → [] = replicate (length.{u} (α := α) []) a
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a
have singleton : ∀ (x : α), IsChain (fun (x1 x2 : α) ↦ x1 = x2) [x] ↔ ∀ (a : α), a ∈ [x].head? → [x] = replicate [x].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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ IsChain (fun (x1 x2 : α) ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a
have 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
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
l : List.chains r
acc : ∀ (a : α), a ∈ (↑l : List α).head? → Acc r a
⊢ Acc (List.lex_chains r) l
have 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)
Tactic: obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
Cleared hypotheses: l, acc
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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)
⊢ Acc (List.lex_chains r) l
have 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)
Tactic: obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
Cleared hypotheses: l, acc
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hl)
have 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
Tactic: apply Acc.intro
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
have cons : a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head?
Tactic: specialize acc a _
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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?
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
have cons₁ : ∀ (acc : Acc r a), Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
Tactic: specialize acc a _
Cleared hypotheses: acc
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head?
have cons : a ∈ some a
Tactic: rw [List.head?_cons, Option.mem_some_iff]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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
⊢ a ∈ (↑(Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl) : List α).head?
have cons₁ : a = a
Tactic: rw [List.head?_cons, Option.mem_some_iff]
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
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)
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
have hl' : List.IsChain (flip r) l
Tactic: have hl' := (List.isChain_cons.1 hl).2
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
have 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'
Tactic: rcases l with - | ⟨b, l⟩
Cleared hypotheses: l, hl, hl', l'
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
⊢ Acc (List.lex_chains r) l'
have 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'
Tactic: rcases l with - | ⟨b, l⟩
Cleared hypotheses: l, hl, hl', l'
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
⊢ Acc (List.lex_chains r) l'
have nil : ∀ (y : List.chains r), List.lex_chains r y l' → Acc (List.lex_chains r) y
Tactic: apply Acc.intro
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
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) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
have this : 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
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
have 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)
Tactic: revert hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
⊢ ∀ (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)
have 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)
Tactic: rw [(by rfl : l = l'.1)]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
⊢ ∀ (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)
have 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)
Tactic: clear_value l'
Cleared hypotheses: l', this
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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 α))
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l : List α)) hl)
have 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
Tactic: apply Acc.intro