awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
a b : ℕ
⊢ range' a b 0 = replicate b a
have zero : range' a 0 0 = replicate 0 a
Tactic: induction b with
  | zero => simp
  | succ b ih => simp [range'_succ, ih, replicate_succ]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
a b : ℕ
zero : range' a 0 0 = replicate 0 a
⊢ range' a b 0 = replicate b a
have succ : ∀ (b : ℕ) (ih : range' a b 0 = replicate b a), range' a (b + 1) 0 = replicate (b + 1) a
Tactic: induction b with
  | zero => simp
  | succ b ih => simp [range'_succ, ih, replicate_succ]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
a b s x : ℕ
hx : x ∈ range' a b s
⊢ a ≤ x
have obtain : ∀ (i : ℕ), i < b → ∀ (hx : a + s * i ∈ range' a b s), a ≤ a + s * i
Tactic: obtain ⟨i, _, rfl⟩ := List.mem_range'.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
⊢ (a :: l = [] ∨
      (∃ (a_1 : α), a :: l = [a_1]) ∨
        ∃ (a_1 : α), ∃ (b : α), ∃ (l_1 : List α), R a_1 b ∧ IsChain R (b :: l_1) ∧ a :: l = a_1 :: b :: l_1) ↔
    l = [] ∨ ∃ (b : α), ∃ (l' : List α), R a b ∧ IsChain R (b :: l') ∧ l = b :: l'
have simp : (l = [] ∨ ∃ (a_1 : α), ∃ (b : α), R a_1 b ∧ ∃ (x : List α), IsChain R (b :: x) ∧ a = a_1 ∧ l = b :: x) ↔
  l = [] ∨ ∃ (b : α), R a b ∧ ∃ (x : List α), IsChain R (b :: x) ∧ l = b :: x
Tactic: simp only [cons_ne_nil, List.cons_eq_cons, exists_and_right,
      exists_eq', true_and, exists_and_left, false_or]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b
p : IsChain R l
⊢ IsChain S l
have nil : ∀ (H : ∀ (a b : α), Membership.mem (γ := List α) [] a → Membership.mem (γ := List α) (tail []) b → R a b → S a b),
  IsChain S []
Tactic: induction p with grind
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b
p : IsChain R l
nil :
  ∀ (H : ∀ (a b : α), Membership.mem (γ := List α) [] a → Membership.mem (γ := List α) (tail []) b → R a b → S a b),
    IsChain S []
⊢ IsChain S l
have singleton : ∀ (a : α) (H : ∀ (a_1 b : α), a_1 ∈ [a] → b ∈ [a].tail → R a_1 b → S a_1 b), IsChain S [a]
Tactic: induction p with grind
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R S : α → α → Prop
l : List α
H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b
p : IsChain R l
nil :
  ∀ (H : ∀ (a b : α), Membership.mem (γ := List α) [] a → Membership.mem (γ := List α) (tail []) b → R a b → S a b),
    IsChain S []
singleton : ∀ (a : α) (H : ∀ (a_1 b : α), a_1 ∈ [a] → b ∈ [a].tail → R a_1 b → S a_1 b), IsChain S [a]
⊢ IsChain S l
have cons_cons : ∀ {a b : α} {l : List α},
  R a b →
    IsChain R (b :: l) →
      (∀ (H : ∀ (a b_1 : α), a ∈ b :: l → b_1 ∈ (b :: l).tail → R a b_1 → S a b_1), IsChain S (b :: l)) →
        ∀ (H : ∀ (a_1 b_1 : α), a_1 ∈ a :: b :: l → b_1 ∈ (a :: b :: l).tail → R a_1 b_1 → S a_1 b_1),
          IsChain S (a :: b :: l)
Tactic: induction p with grind
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)
have nil : ∀ {l₂ : List α}, IsChain R ([] ++ c :: l₂) ↔ IsChain R ([] ++ [c]) ∧ IsChain R (c :: l₂)
Tactic: induction l₁ using twoStepInduction generalizing l₂ with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
c : α
l₁ l₂ : List α
nil : ∀ {l₂ : List α}, IsChain R ([] ++ c :: l₂) ↔ IsChain R ([] ++ [c]) ∧ IsChain R (c :: l₂)
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)
have singleton : ∀ (x : α) {l₂ : List α}, IsChain R ([x] ++ c :: l₂) ↔ IsChain R ([x] ++ [c]) ∧ IsChain R (c :: l₂)
Tactic: induction l₁ using twoStepInduction generalizing l₂ with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
c : α
l₁ l₂ : List α
nil : ∀ {l₂ : List α}, IsChain R ([] ++ c :: l₂) ↔ IsChain R ([] ++ [c]) ∧ IsChain R (c :: l₂)
singleton : ∀ (x : α) {l₂ : List α}, IsChain R ([x] ++ c :: l₂) ↔ IsChain R ([x] ++ [c]) ∧ IsChain R (c :: l₂)
⊢ IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)
have cons_cons : ∀ (x y : α) (xs : List α),
  (∀ {l₂ : List α}, IsChain R (xs ++ c :: l₂) ↔ IsChain R (xs ++ [c]) ∧ IsChain R (c :: l₂)) →
    (∀ (y : α) {l₂ : List α}, IsChain R (y :: xs ++ c :: l₂) ↔ IsChain R (y :: xs ++ [c]) ∧ IsChain R (c :: l₂)) →
      ∀ {l₂ : List α}, IsChain R (x :: y :: xs ++ c :: l₂) ↔ IsChain R (x :: y :: xs ++ [c]) ∧ IsChain R (c :: l₂)
Tactic: induction l₁ using twoStepInduction generalizing l₂ with grind
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
b c : α
l₁ l₂ : List α
⊢ IsChain R (l₁ ++ b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
have rw : IsChain R (l₁ ++ [b]) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
Tactic: rw [isChain_split, isChain_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
b c : α
l₁ l₂ : List α
rw : IsChain R (l₁ ++ [b]) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
⊢ IsChain R (l₁ ++ b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
have rw₁ : IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)
Tactic: rw [isChain_split, isChain_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b c : α
l₁ l₂ : List α
⊢ IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
have rw : IsChain R (a :: (l₁ ++ [b])) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
Tactic: rw [isChain_cons_split, isChain_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b c : α
l₁ l₂ : List α
rw :
  IsChain R (a :: (l₁ ++ [b])) ∧ IsChain R (b :: c :: l₂) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
⊢ IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
have rw₁ : IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)
Tactic: rw [isChain_cons_split, isChain_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b
have refine : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l
Tactic: refine ⟨fun h _ _ _ _ eq => (isChain_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (head :: head' :: tail)
have cons_cons : ∀ (h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄
  (eq : head' :: tail = l₁ ++ a :: b :: l₂), R a b
Tactic: refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h_1 : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ R a b
have cons_cons : head :: head' :: tail = head :: l₁ ++ a :: b :: l₂
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h_1 : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ head :: head' :: tail = head :: l₁ ++ a :: b :: l₂
have cons_cons : head :: (l₁ ++ a :: b :: l₂) = head :: l₁ ++ a :: b :: l₂
Tactic: rw [eq, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
head head' : α
tail : List α
h_1 : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
cons_cons : head :: (l₁ ++ a :: b :: l₂) = head :: l₁ ++ a :: b :: l₂
⊢ head :: head' :: tail = head :: l₁ ++ a :: b :: l₂
have cons_cons₁ : head :: (l₁ ++ a :: b :: l₂) = head :: (l₁ ++ a :: b :: l₂)
Tactic: rw [eq, cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l
have nil : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []
Tactic: induction l using twoStepInduction with
  | nil | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l
have singleton : ∀ (x : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [x] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R [x]
Tactic: induction l using twoStepInduction with
  | nil | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R []
singleton : ∀ (x : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, [x] = l₁ ++ a :: b :: l₂ → R a b) → IsChain R [x]
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l
have cons_cons : ∀ (head head' : α) (tail : List α),
  ((∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail) →
    ∀ (ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)),
      (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b) →
        IsChain R (head :: head' :: tail)
Tactic: induction l using twoStepInduction with
  | nil | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail
have nil : IsChain R [] ↔ Forall₂ R (dropLast []) (tail [])
Tactic: induction l using twoStepInduction
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : IsChain R [] ↔ Forall₂ R (dropLast []) (tail [])
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail
have singleton : ∀ (x : α), IsChain R [x] ↔ Forall₂ R [x].dropLast [x].tail
Tactic: induction l using twoStepInduction
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
nil : IsChain R [] ↔ Forall₂ R (dropLast []) (tail [])
singleton : ∀ (x : α), IsChain R [x] ↔ Forall₂ R [x].dropLast [x].tail
⊢ IsChain R l ↔ Forall₂ R l.dropLast l.tail
have cons_cons : ∀ (x y : α) (xs : List α),
  (IsChain R xs ↔ Forall₂ R xs.dropLast xs.tail) →
    (∀ (y : α), IsChain R (y :: xs) ↔ Forall₂ R (y :: xs).dropLast (y :: xs).tail) →
      (IsChain R (x :: y :: xs) ↔ Forall₂ R (x :: y :: xs).dropLast (x :: y :: xs).tail)
Tactic: induction l using twoStepInduction
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
a : α
⊢ IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l
have nil : IsChain R [a] ↔ Eq.{u + 1} (α := List α) [] [] ∨ Forall₂ R (a :: dropLast []) []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
a : α
nil : IsChain R [a] ↔ Eq.{u + 1} (α := List α) [] [] ∨ Forall₂ R (a :: dropLast []) []
⊢ IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l
have cons : ∀ (head : α) (tail : List α),
  IsChain R (a :: head :: tail) ↔ head :: tail = [] ∨ Forall₂ R (a :: (head :: tail).dropLast) (head :: tail)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])
have simp_rw : Forall₂ R (a :: l ++ [b]).dropLast (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
Tactic: simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
simp_rw : Forall₂ R (a :: l ++ [b]).dropLast (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])
have simp_rw₁ : Forall₂ R (a :: l) (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
Tactic: simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
simp_rw : Forall₂ R (a :: l ++ [b]).dropLast (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
simp_rw₁ : Forall₂ R (a :: l) (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])
have simp_rw₂ : Forall₂ R (a :: l) (a :: (l ++ [b])).tail ↔ Forall₂ R (a :: l) (l ++ [b])
Tactic: simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
l : List β
⊢ IsChain R (map f l) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) l
have nil : IsChain R (map f []) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) []
Tactic: induction l using twoStepInduction
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
l : List β
nil : IsChain R (map f []) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) []
⊢ IsChain R (map f l) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) l
have singleton : ∀ (x : β), IsChain R (map f [x]) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) [x]
Tactic: induction l using twoStepInduction
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
l : List β
nil : IsChain R (map f []) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) []
singleton : ∀ (x : β), IsChain R (map f [x]) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) [x]
⊢ IsChain R (map f l) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) l
have cons_cons : ∀ (x y : β) (xs : List β),
  (IsChain R (map f xs) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) xs) →
    (∀ (y : β), IsChain R (map f (y :: xs)) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (y :: xs)) →
      (IsChain R (map f (x :: y :: xs)) ↔ IsChain (fun (a b : β) ↦ R (f a) (f b)) (x :: y :: xs))
Tactic: induction l using twoStepInduction
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
⊢ IsChain S (pmap (P := p) f l hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) l
have nil : ∀ (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
  IsChain S (pmap (P := p) f [] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) []
Tactic: induction l using twoStepInduction
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
nil :
  ∀ (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
    IsChain S (pmap (P := p) f [] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) []
⊢ IsChain S (pmap (P := p) f l hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) l
have singleton : ∀ (x : α) (hl : ∀ (a : α), a ∈ [x] → p a),
  IsChain S (pmap (P := p) f [x] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) [x]
Tactic: induction l using twoStepInduction
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
β : Type v
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
nil :
  ∀ (hl : ∀ (a : α), Membership.mem (γ := List α) [] a → p a),
    IsChain S (pmap (P := p) f [] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) []
singleton :
  ∀ (x : α) (hl : ∀ (a : α), a ∈ [x] → p a),
    IsChain S (pmap (P := p) f [x] hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) [x]
⊢ IsChain S (pmap (P := p) f l hl) ↔ IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) l
have cons_cons : ∀ (x y : α) (xs : List α),
  (∀ (hl : ∀ (a : α), a ∈ xs → p a),
      IsChain S (pmap (P := p) f xs hl) ↔
        IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) xs) →
    (∀ (y : α) (hl : ∀ (a : α), a ∈ y :: xs → p a),
        IsChain S (pmap (P := p) f (y :: xs) hl) ↔
          IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) (y :: xs)) →
      ∀ (hl : ∀ (a : α), a ∈ x :: y :: xs → p a),
        IsChain S (pmap (P := p) f (x :: y :: xs) hl) ↔
          IsChain (fun (a b : α) ↦ ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) (x :: y :: xs)
Tactic: induction l using twoStepInduction
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst : Trans R R R
hl : IsChain R l₂
h : l₁ <+ l₂
⊢ IsChain R l₁
have rw : ∀ (hl : Pairwise R l₂) (h : l₁ <+ l₂), Pairwise R l₁
Tactic: rw [isChain_iff_pairwise] at hl ⊢
Cleared hypotheses: hl, h
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
R : α → α → Prop
l : List α
a b : α
inst : Trans R R R
hl : IsChain R (a :: l)
hb : b ∈ l
⊢ R a b
have hl₁ : Pairwise R (a :: l)
Tactic: rw [isChain_iff_pairwise] at hl
Cleared hypotheses: hl, hb
-- Lean 4 proof step from Mathlib.Data.List.Chain (hypothesis)
Goal:
α : Type u
R : α → α → Prop
x : α
l : List α
h : IsChain R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y
have h₁ : IsChain R (x :: y :: l.tail)
Tactic: rw [← cons_head?_tail hy] at h
Cleared hypotheses: h, hy
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ IsChain R (a :: b :: l₁ ++ l₂) ↔
    IsChain R (a :: b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
have rw : (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
  R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
Tactic: rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons,
      ← cons_append, isChain_append, and_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u
R : α → α → Prop
l l₁ : List α
h : IsChain R l
h' : l₁ <:+: l
⊢ IsChain R l₁
have rcases : ∀ (l₂ l₃ : List α) (h : IsChain R (l₂ ++ l₁ ++ l₃)), IsChain R l₁
Tactic: rcases h' with ⟨l₂, l₃, rfl⟩
Cleared hypotheses: l, h, h'
-- 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)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons : IsChain R (a :: b :: l).reverse ↔ 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)
⊢ IsChain R (a :: b :: l).reverse ↔ IsChain (fun (a b : α) ↦ R b a) (a :: b :: l)
have cons_cons₁ : IsChain R ((b :: l).reverse ++ [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)
⊢ 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)
⊢ 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]