awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₆ : IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₆ : IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₇ : IsChain R (b :: l).reverse ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₆ : IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₇ : IsChain R (b :: l).reverse ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₈ : IsChain (fun (a b : α) ↦ R b a) (b :: l) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₆ : IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₇ : IsChain R (b :: l).reverse ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₈ :
  IsChain (fun (a b : α) ↦ R b a) (b :: l) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₉ : IsChain R [b, a] ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)
cons_cons : IsChain R (a :: b :: l).reverse ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₁ : IsChain R ((b :: l).reverse ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₂ : IsChain R (l.reverse ++ [b] ++ [a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₃ : IsChain R (l.reverse ++ ([b] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₄ : IsChain R (l.reverse ++ b :: ([] ++ [a])) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₅ : IsChain R (l.reverse ++ [b, a]) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₆ : IsChain R (l.reverse ++ [b]) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₇ : IsChain R (b :: l).reverse ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₈ :
  IsChain (fun (a b : α) ↦ R b a) (b :: l) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
cons_cons₉ :
  IsChain R [b, a] ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₁₀ : R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l) ↔ R b a ∧ IsChain (fun (a b : α) ↦ R b a) (b :: l)
Tactic: rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
have nil : IsChain R (reverse []) ↔ IsChain (fun (a b : α) ↦ R b a) []
Tactic: induction l using twoStepInduction with
  | nil => grind
  | singleton a => grind
  | cons_cons a b l IH IH2 =>
    rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : IsChain R (reverse []) ↔ IsChain (fun (a b : α) ↦ R b a) []
⊢ IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
have singleton : ∀ (a : α), IsChain R [a].reverse ↔ IsChain (fun (a b : α) ↦ R b a) [a]
Tactic: induction l using twoStepInduction with
  | nil => grind
  | singleton a => grind
  | cons_cons a b l IH IH2 =>
    rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : IsChain R (reverse []) ↔ IsChain (fun (a b : α) ↦ R b a) []
singleton : ∀ (a : α), IsChain R [a].reverse ↔ IsChain (fun (a b : α) ↦ R b a) [a]
⊢ IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l
have cons_cons : ∀ (a b : α) (l : List α) (IH : IsChain R l.reverse ↔ IsChain (fun (a b : α) ↦ R b a) l)
  (IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (y :: l)),
  IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
Tactic: induction l using twoStepInduction with
  | nil => grind
  | singleton a => grind
  | cons_cons a b l IH IH2 =>
    rw [isChain_cons_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      isChain_split, ← reverse_cons, IH2, and_comm, isChain_pair]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬[] ∈ l₁ :: l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
have hL₁ : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
Tactic: rw [mem_cons, not_or, ← Ne] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)
have rw : (IsChain R l₁ ∧
    ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
        IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
      ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
  (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
    (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
      IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
Tactic: rw [flatten_cons, isChain_append, isChain_flatten hL.2, forall_mem_cons, isChain_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
have hL₁ : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
Tactic: rw [mem_cons, not_or, ← Ne] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
have simp : (IsChain R l₁ ∧
    IsChain R l₂ ∧
      (∀ (x : List α), x ∈ L → IsChain R x) ∧
        IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
          ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
  IsChain R l₁ ∧
    IsChain R l₂ ∧
      (∀ (x : List α), x ∈ L → IsChain R x) ∧
        (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
Tactic: simp only [forall_mem_cons, and_assoc, flatten_cons, head?_append_of_ne_nil _ hL.2.1.symm]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
l : List α
p : α → Prop
h : ∀ (x : α), x ∈ l → p x
r : { a : α // p a } → { a : α // p a } → Prop
⊢ IsChain r (l.attachWith p h) ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : p a),
          ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
      l
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
  IsChain r (attachWith [] p h) ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : p a),
          ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
      []
Tactic: induction l with grind +splitIndPred
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
l : List α
p : α → Prop
h : ∀ (x : α), x ∈ l → p x
r : { a : α // p a } → { a : α // p a } → Prop
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
    IsChain r (attachWith [] p h) ↔
      IsChain
        (fun (a b : α) ↦
          ∃ (ha : p a),
            ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
        []
⊢ IsChain r (l.attachWith p h) ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : p a),
          ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
      l
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ (x : α), x ∈ tail → p x),
      IsChain r (tail.attachWith p h) ↔
        IsChain
          (fun (a b : α) ↦
            ∃ (ha : p a),
              ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
          tail) →
    ∀ (h : ∀ (x : α), x ∈ head :: tail → p x),
      IsChain r ((head :: tail).attachWith p h) ↔
        IsChain
          (fun (a b : α) ↦
            ∃ (ha : p a),
              ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
          (head :: tail)
Tactic: induction l with grind +splitIndPred
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ (l : List α), IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
have refine_1 : ∃ (l : List α), IsChain r (b :: l) ∧ (b :: l).getLast sorry = b
Tactic: refine Relation.ReflTransGen.head_induction_on h ?_ ?_
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
refine_1 : ∃ (l : List α), IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
have refine_2 : ∀ {a c : α} (h' : r a c) (h : Relation.ReflTransGen r c b),
  (∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast sorry = b) →
    ∃ (l : List α), IsChain r (a :: l) ∧ (a :: l).getLast sorry = b
Tactic: refine Relation.ReflTransGen.head_induction_on h ?_ ?_
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h_1 : Relation.ReflTransGen r d b
ih : ∃ (l : List α), IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
have refine_2 : ∀ (l : List α) (hl₁ : IsChain r (d :: l)) (hl₂ : (d :: l).getLast sorry = b),
  ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast sorry = b
Tactic: obtain ⟨l, hl₁, hl₂⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h_1 : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
have refine_2 : (c :: d :: l).getLast sorry = b
Tactic: refine ⟨d :: l, .cons_cons e hl₁, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b
have rcases : ∀ (l : List α),
  IsChain r (a :: l) ∧ (a :: l).getLast sorry = b →
    ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b
Tactic: rcases exists_isChain_cons_of_relationReflTransGen h with ⟨l, _⟩
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
⊢ ∀ (i : α), i ∈ l → p i
have nil : ∀ (h : IsChain r []) (initial : ∀ (lne : Ne.{u + 1} (α := List α) [] []), p (head [] lne)) (i : α),
  Membership.mem (γ := List α) [] i → p i
Tactic: induction l using twoStepInduction with grind
Cleared hypotheses: l, h, initial
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
nil :
  ∀ (h : IsChain r []) (initial : ∀ (lne : Ne.{u + 1} (α := List α) [] []), p (head [] lne)) (i : α),
    Membership.mem (γ := List α) [] i → p i
⊢ ∀ (i : α), i ∈ l → p i
have singleton : ∀ (x : α) (h : IsChain r [x]) (initial : ∀ (lne : [x] ≠ []), p ([x].head lne)) (i : α), i ∈ [x] → p i
Tactic: induction l using twoStepInduction with grind
Cleared hypotheses: l, h, initial
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
nil :
  ∀ (h : IsChain r []) (initial : ∀ (lne : Ne.{u + 1} (α := List α) [] []), p (head [] lne)) (i : α),
    Membership.mem (γ := List α) [] i → p i
singleton : ∀ (x : α) (h : IsChain r [x]) (initial : ∀ (lne : [x] ≠ []), p ([x].head lne)) (i : α), i ∈ [x] → p i
⊢ ∀ (i : α), i ∈ l → p i
have cons_cons : ∀ (x y : α) (xs : List α),
  (∀ (h : IsChain r xs) (initial : ∀ (lne : xs ≠ []), p (xs.head lne)) (i : α), i ∈ xs → p i) →
    (∀ (y : α) (h : IsChain r (y :: xs)) (initial : ∀ (lne : y :: xs ≠ []), p ((y :: xs).head lne)) (i : α),
        i ∈ y :: xs → p i) →
      ∀ (h : IsChain r (x :: y :: xs)) (initial : ∀ (lne : x :: y :: xs ≠ []), p ((x :: y :: xs).head lne)) (i : α),
        i ∈ x :: y :: xs → p i
Tactic: induction l using twoStepInduction with grind
Cleared hypotheses: l, h, initial
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
⊢ ∀ (i : α), i ∈ l → p i
have H : IsChain (flip (flip r)) l
Tactic: have H : IsChain (flip (flip r)) l := h
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
H : IsChain (flip (flip r)) l
⊢ ∀ (i : α), i ∈ l → p i
have H₁ : ∀ (initial : ∀ (lne : l.reverse ≠ []), p (l.reverse.head lne)) (i : α), i ∈ l.reverse → p i
Tactic: replace H := (isChain_reverse.mpr H).induction _ _ (fun _ _ h ↦ carries h)
Cleared hypotheses: H
-- 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
⊢ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: b :: bs)
have cons : a > b
Tactic: apply hm.cons_cons
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]
hmas : b :: bs ≤ []
⊢ a > b
have hmas₁ : b :: bs < []
Tactic: simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
Cleared hypotheses: hmas
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b
have ha₁ : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
Tactic: rw [List.isChain_cons_cons] at ha
Cleared hypotheses: ha, 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
⊢ a > b
have cons : b ≤ a'
Tactic: refine lt_of_le_of_lt ?_ ha.1
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
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 ≤ a'
have hmas₁ : b :: bs < a' :: as ∨ b :: bs = a' :: as
Tactic: rw [le_iff_lt_or_eq] at hmas
Cleared hypotheses: hmas