awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
a : α
l : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) b
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (a :: l) ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
have cons : ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) []),
  (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (a :: l) ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      []
Tactic: rcases b with - | ⟨b, m⟩
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
a : α
l : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) b
cons :
  ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) []),
    (fun (l : List α) ↦
          (match (motive := List α → Prop) l with
            | [] => True
            | a :: m => IsChain r (a :: m ++ [a]) :
            Prop))
        (a :: l) ↔
      (fun (l : List α) ↦
          (match (motive := List α → Prop) l with
            | [] => True
            | a :: m => IsChain r (a :: m ++ [a]) :
            Prop))
        []
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (a :: l) ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
have cons₁ : ∀ (b : α) (m : List α) (hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) (b :: m)),
  (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (a :: l) ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (b :: m)
Tactic: rcases b with - | ⟨b, m⟩
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α : List α → List α → Prop) [] (b :: m)
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      [] ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (b :: m)
have this : [] = b :: m
Tactic: have := isRotated_nil_iff'.1 hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) []
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (a :: l) ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      []
have this : a :: l = []
Tactic: have := isRotated_nil_iff.1 hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) (b :: m)
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons : ∀ (n : ℕ) (hn : (a :: l).rotate n = b :: m), IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
Tactic: obtain ⟨n, hn⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate 0 = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have hn₁ : a = b ∧ l = m
Tactic: simp only [rotate_zero, cons.injEq] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : a = b ∧ l = m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons : IsChain r (b :: l ++ [b]) ↔ IsChain r (b :: m ++ [b])
Tactic: rw [hn.1, hn.2]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : a = b ∧ l = m
cons : IsChain r (b :: l ++ [b]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons₁ : IsChain r (b :: m ++ [b]) ↔ IsChain r (b :: m ++ [b])
Tactic: rw [hn.1, hn.2]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate (d + 1) = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons : ∀ (hn : [a].rotate (d + 1) = b :: m), IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])
Tactic: rcases l with - | ⟨c, s⟩
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate (d + 1) = b :: m
cons : ∀ (hn : [a].rotate (d + 1) = b :: m), IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons₁ : ∀ (c : α) (s : List α) (hn : (a :: c :: s).rotate (d + 1) = b :: m),
  IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
Tactic: rcases l with - | ⟨c, s⟩
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a b : α
m : List α
hn : [a].rotate (d + 1) = b :: m
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])
have hn₁ : a = b ∧ [] = m
Tactic: simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a b : α
m : List α
hn : a = b ∧ [] = m
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons : IsChain r ([b] ++ [b]) ↔ IsChain r (b :: m ++ [b])
Tactic: rw [hn.1, hn.2]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a b : α
m : List α
hn : a = b ∧ [] = m
cons : IsChain r ([b] ++ [b]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons₁ : IsChain r (b :: m ++ b :: m) ↔ IsChain r (b :: m ++ b :: m)
Tactic: rw [hn.1, hn.2]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
c_1 : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
have hn₁ : (c :: (s ++ [a])).rotate d = b :: m
Tactic: rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c_1 : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
a b : α
m : List α
c : α
s : List α
hn : (c :: (s ++ [a])).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons : IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (c :: (s ++ [a]) ++ [c])
Tactic: rw [← hd c _ _ _ hn]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
n : ℕ
hn : (a :: l).rotate n = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons : ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate 0 = b :: m),
  IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
Tactic: induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]
Cleared hypotheses: a, l, b, m, n, hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
n : ℕ
hn : (a :: l).rotate n = b :: m
cons :
  ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate 0 = b :: m),
    IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
have cons₁ : ∀ (d : ℕ)
  (hd :
    ∀ (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate d = b :: m),
      IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
  (a : α) (l : List α) (b : α) (m : List α) (hn : (a :: l).rotate (d + 1) = b :: m),
  IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
Tactic: induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]
Cleared hypotheses: a, l, b, m, n, hn
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r (↑[a] : Cycle α) ↔ r a a
have rw : IsChain r (a :: ([] ++ [a])) ↔ r a a
Tactic: rw [chain_coe_cons, nil_append, List.isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
a : α
rw : IsChain r (a :: ([] ++ [a])) ↔ r a a
⊢ Chain r (↑[a] : Cycle α) ↔ r a a
have rw₁ : IsChain r [a, a] ↔ r a a
Tactic: rw [chain_coe_cons, nil_append, List.isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
a : α
rw : IsChain r (a :: ([] ++ [a])) ↔ r a a
rw₁ : IsChain r [a, a] ↔ r a a
⊢ Chain r (↑[a] : Cycle α) ↔ r a a
have rw₂ : r a a ↔ r a a
Tactic: rw [chain_coe_cons, nil_append, List.isChain_pair]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r (↑m : Cycle α) ↔ IsChain r (m.getLast hl :: m)
hl : m ++ [a] ≠ []
⊢ Chain r (↑(m ++ [a]) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
have rw : Chain r (↑(a :: m) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
Tactic: rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r (↑m : Cycle α) ↔ IsChain r (m.getLast hl :: m)
hl : m ++ [a] ≠ []
rw : Chain r (↑(a :: m) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
⊢ Chain r (↑(m ++ [a]) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
have rw₁ : IsChain r (a :: (m ++ [a])) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
Tactic: rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r (↑m : Cycle α) ↔ IsChain r (m.getLast hl :: m)
hl : m ++ [a] ≠ []
rw : Chain r (↑(a :: m) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
rw₁ : IsChain r (a :: (m ++ [a])) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
⊢ Chain r (↑(m ++ [a]) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
have rw₂ : IsChain r (a :: (m ++ [a])) ↔ IsChain r (a :: (m ++ [a]))
Tactic: rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦l⟧
have nil : Chain r (map f ⟦[]⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦[]⟧
Tactic: rcases l with - | ⟨a, l⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
nil : Chain r (map f ⟦[]⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦[]⟧
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦l⟧
have cons : ∀ (a : β) (l : List β), Chain r (map f ⟦a :: l⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦a :: l⟧
Tactic: rcases l with - | ⟨a, l⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r (↑(range n.succ) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
have rw : Chain r (↑(range n ++ [n]) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Tactic: rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
rw : Chain r (↑(range n ++ [n]) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
⊢ Chain r (↑(range n.succ) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
have rw₁ : Chain r (↑(n :: range n) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Tactic: rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
rw : Chain r (↑(range n ++ [n]) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
rw₁ : Chain r (↑(n :: range n) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
⊢ Chain r (↑(range n.succ) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
have rw₂ : IsChain r (n :: (range n ++ [n])) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Tactic: rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
rw : Chain r (↑(range n ++ [n]) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
rw₁ : Chain r (↑(n :: range n) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
rw₂ : IsChain r (n :: (range n ++ [n])) ↔ r n 0 ∧ ∀ m < n, r m m.succ
⊢ Chain r (↑(range n.succ) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
have rw₃ : IsChain r (n :: range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Tactic: rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
r : ℕ → ℕ → Prop
n : ℕ
rw : Chain r (↑(range n ++ [n]) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
rw₁ : Chain r (↑(n :: range n) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
rw₂ : IsChain r (n :: (range n ++ [n])) ↔ r n 0 ∧ ∀ m < n, r m m.succ
rw₃ : IsChain r (n :: range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
⊢ Chain r (↑(range n.succ) : Cycle ℕ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
have rw₄ : (r n 0 ∧ ∀ m < n, r m m.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Tactic: rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s
have nil : ∀ (p : Chain r₁ Cycle.nil), Chain r₂ Cycle.nil
Tactic: induction s
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
nil : ∀ (p : Chain r₁ Cycle.nil), Chain r₂ Cycle.nil
⊢ Chain r₂ s
have cons : ∀ (a : α) (l : List α),
  (∀ (p : Chain r₁ (↑l : Cycle α)), Chain r₂ (↑l : Cycle α)) →
    ∀ (p : Chain r₁ (↑(a :: l) : Cycle α)), Chain r₂ (↑(a :: l) : Cycle α)
Tactic: induction s
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a : α
l : List α
h : ∀ (p : Chain r₁ (↑l : Cycle α)), Chain r₂ (↑l : Cycle α)
p : Chain r₁ (↑(a :: l) : Cycle α)
⊢ Chain r₂ (↑(a :: l) : Cycle α)
have p₁ : IsChain r₁ (a :: (l ++ [a]))
Tactic: rw [chain_coe_cons] at p ⊢
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s
have cons : ∀ (a : α) (l : List α),
  ((∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b) → Chain r (↑l : Cycle α)) →
    (∀ a_2 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_2 b) → Chain r (↑(a :: l) : Cycle α)
Tactic: induction s with
  | nil => exact fun _ ↦ Cycle.Chain.nil r
  | cons a l => ?_
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
h : (∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b) → Chain r (↑l : Cycle α)
hs : ∀ a_1 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_1 b
⊢ Chain r (↑(a :: l) : Cycle α)
have Ha : a ∈ (↑(a :: l) : Cycle α)
Tactic: have Ha : a ∈ (a :: l : Cycle α) := by simp
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
h : (∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b) → Chain r (↑l : Cycle α)
hs : ∀ a_1 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_1 b
Ha : a ∈ (↑(a :: l) : Cycle α)
⊢ Chain r (↑(a :: l) : Cycle α)
have Hl : ∀ {b : α} (_hb : b ∈ l), b ∈ (↑(a :: l) : Cycle α)
Tactic: have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
h : (∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b) → Chain r (↑l : Cycle α)
hs : ∀ a_1 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_1 b
Ha : a ∈ (↑(a :: l) : Cycle α)
Hl : ∀ {b : α} (_hb : b ∈ l), b ∈ (↑(a :: l) : Cycle α)
⊢ IsChain r (a :: (l ++ [a]))
have cons : List.Pairwise r (a :: (l ++ [a]))
Tactic: apply Pairwise.isChain
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
h : (∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b) → Chain r (↑l : Cycle α)
hs : ∀ a_1 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_1 b
Ha : a ∈ (↑(a :: l) : Cycle α)
Hl : ∀ {b : α} (_hb : b ∈ l), b ∈ (↑(a :: l) : Cycle α)
⊢ List.Pairwise r (a :: (l ++ [a]))
have cons : (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])
Tactic: rw [pairwise_cons]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b
have cons : ∀ (a : α) (l : List α),
  (Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b) →
    Chain r (↑(a :: l) : Cycle α) → ∀ a_3 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_3 b
Tactic: induction s with
    | nil => exact fun _ b hb ↦ (notMem_nil _ hb).elim
    | cons a l => ?_
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
hs : Chain r (↑(a :: l) : Cycle α)
b : α
hb : b ∈ (↑(a :: l) : Cycle α)
c : α
hc : c ∈ (↑(a :: l) : Cycle α)
⊢ r b c
have cons : ∀ (hs : List.Pairwise r (a :: (l ++ [a]))) (b : α) (hb : b ∈ (↑(a :: l) : Cycle α)) (c : α)
  (hc : c ∈ (↑(a :: l) : Cycle α)), r b c
Tactic: rw [Cycle.chain_coe_cons, List.isChain_iff_pairwise] at hs
Cleared hypotheses: hs, b, hb, c, hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
hs : List.Pairwise r (a :: (l ++ [a]))
b : α
hb : b ∈ (↑(a :: l) : Cycle α)
c : α
hc : c ∈ (↑(a :: l) : Cycle α)
⊢ r b c
have hs₁ : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
Tactic: simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil,
      IsEmpty.forall_iff, imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b : α
hb : b ∈ (↑(a :: l) : Cycle α)
c : α
hc : c ∈ (↑(a :: l) : Cycle α)
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
⊢ r b c
have hb₁ : b = a ∨ b ∈ l
Tactic: simp only [mem_coe_iff, mem_cons] at hb hc
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b : α
hb : b ∈ (↑(a :: l) : Cycle α)
c : α
hc : c ∈ (↑(a :: l) : Cycle α)
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb₁ : b = a ∨ b ∈ l
⊢ r b c
have hc₁ : c = a ∨ c ∈ l
Tactic: simp only [mem_coe_iff, mem_cons] at hb hc
Cleared hypotheses: hb, hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b = a ∨ b ∈ l
hc : c = a ∨ c ∈ l
⊢ r b c
have cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b) (hc : c = b ∨ c ∈ l), r b c
Tactic: rcases hb with (rfl | hb)
Cleared hypotheses: a, hs, hb, hc
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
a : α
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b = a ∨ b ∈ l
hc : c = a ∨ c ∈ l
cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b) (hc : c = b ∨ c ∈ l), r b c
⊢ r b c
have cons₁ : ∀ (hb : b ∈ l), r b c
Tactic: rcases hb with (rfl | hb)
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
l : List α
h : Chain r (↑l : Cycle α) → ∀ a ∈ (↑l : Cycle α), ∀ b ∈ (↑l : Cycle α), r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c = b ∨ c ∈ l
⊢ r b c
have cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c), r c c
Tactic: rcases hc with (rfl | hc)
Cleared hypotheses: b, hs, hc