awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
hab : (IsRotated.setoid α : List α → List α → Prop) [] []
⊢ (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))
      []

Tactic:
rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α : List α → List α → Prop) [] (b :: m)
⊢ [] = b :: m

Tactic:
have := isRotated_nil_iff'.1 hab
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α : List α → List α → Prop) [] (b :: m)
this : [] = 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)

Tactic:
contradiction
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) []
⊢ a :: l = []

Tactic:
have := isRotated_nil_iff.1 hab
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) []
this : 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:
contradiction
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) (b :: m)
cons : ∀ (n : ℕ) (hn : (a :: l).rotate n = b :: m), IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
obtain ⟨n, hn⟩ := hab
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate 0 = b :: m
⊢ a = b ∧ l = m

Tactic:
simp only [rotate_zero, cons.injEq] at hn

Premises used: List.cons.injEq, List.rotate_zero
-- Module: Mathlib.Data.List.Cycle
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])
cons₁ cons₂ : IsChain r (b :: m ++ [b]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rw [hn.1, hn.2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.List.Cycle
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])
cons₁ :
  ∀ (c : α) (s : List α) (hn : (a :: c :: s).rotate (d + 1) = b :: m),
    IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rcases l with - | ⟨c, s⟩
-- Module: Mathlib.Data.List.Cycle
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
⊢ a = b ∧ [] = m

Tactic:
simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn

Premises used: List.rotate_singleton, List.rotate_cons_succ, List.cons.injEq, List.nil_append
-- Module: Mathlib.Data.List.Cycle
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])
cons₁ cons₂ : IsChain r (b :: m ++ b :: m) ↔ IsChain r (b :: m ++ b :: m)
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rw [hn.1, hn.2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.List.Cycle
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
⊢ (c :: (s ++ [a])).rotate d = b :: m

Tactic:
rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn

Premises used: List.rotate_cons_succ, List.rotate_rotate, List.rotate_zero, List.cons_append, Nat.add_comm
-- Module: Mathlib.Data.List.Cycle
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
cons : IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (c :: (s ++ [a]) ++ [c])
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rw [← hd c _ _ _ hn]
-- Module: Mathlib.Data.List.Cycle
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 (c :: (s ++ [a]) ++ [c])

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.List.Cycle
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])
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])
⊢ 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]

Premises used: List.rotate_singleton, List.rotate_cons_succ, List.rotate_rotate, and_comm, List.cons.injEq, List.nil_append, List.rotate_zero, List.cons_append, Nat.add_comm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
⊢ Chain r Cycle.nil

Tactic:
trivial
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
a : α
l : List α
⊢ Chain r (↑(a :: l) : Cycle α) ↔ IsChain r (a :: (l ++ [a]))

Tactic:
Iff.rfl

Premises used: Quotient.liftOn', Iff.rfl, Cycle.Chain, List.append
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
a : α
rw : IsChain r (a :: ([] ++ [a])) ↔ r a a
rw₁ : IsChain r [a, a] ↔ r a a
rw₂ rw₃ : r a a ↔ r a a
⊢ Chain r (↑[a] : Cycle α) ↔ r a a

Tactic:
rw [chain_coe_cons, nil_append, List.isChain_pair]

Premises used: List.isChain_pair, List.nil_append, Cycle.chain_coe_cons
-- Module: Mathlib.Data.List.Cycle
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]))
⊢ ∀ (hl : m ++ [a] ≠ []), Chain r (↑(m ++ [a]) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))

Tactic:
_
-- Module: Mathlib.Data.List.Cycle
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]))
rw₂ rw₃ : IsChain r (a :: (m ++ [a])) ↔ IsChain r (a :: (m ++ [a]))
⊢ Chain r (↑(m ++ [a]) : Cycle α) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))

Tactic:
rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]

Premises used: List.getLast_append_singleton, Cycle.coe_cons_eq_coe_append, Cycle.chain_coe_cons
-- Module: Mathlib.Data.List.Cycle
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)) ⟦[]⟧
cons : ∀ (a : β) (l : List β), Chain r (map f ⟦a :: l⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦a :: l⟧
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦l⟧

Tactic:
rcases l with - | ⟨a, l⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦[]⟧

Tactic:
rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun (a b : β) ↦ r (f a) (f b)) ⟦a :: l⟧

Tactic:
simp [← concat_eq_append, ← map_concat, List.isChain_cons_map f]

Premises used: List.concat_eq_append, List.isChain_cons_map, List.map_concat
-- Module: Mathlib.Data.List.Cycle
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
rw₄ rw₅ : (r n 0 ∧ ∀ m < n, r m m.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

Tactic:
rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, isChain_cons_range_succ]

Premises used: Cycle.coe_cons_eq_coe_append, List.isChain_cons_range_succ, Cycle.chain_coe_cons, List.range_succ
-- Module: Mathlib.Data.List.Cycle
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
cons :
  ∀ (a : α) (l : List α),
    (∀ (p : Chain r₁ (↑l : Cycle α)), Chain r₂ (↑l : Cycle α)) →
      ∀ (p : Chain r₁ (↑(a :: l) : Cycle α)), Chain r₂ (↑(a :: l) : Cycle α)
⊢ Chain r₂ s

Tactic:
induction s
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

Tactic:
trivial
-- Module: Mathlib.Data.List.Cycle
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 α)
⊢ IsChain r₁ (a :: (l ++ [a]))

Tactic:
rw [chain_coe_cons] at p ⊢

Premises used: Cycle.chain_coe_cons
-- Module: Mathlib.Data.List.Cycle
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 : IsChain r₁ (a :: (l ++ [a]))
⊢ IsChain r₂ (a :: (l ++ [a]))

Tactic:
p.imp H

Premises used: List.IsChain.imp
-- Module: Mathlib.Data.List.Cycle
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 : IsChain r₁ (a :: (l ++ [a]))
⊢ IsChain r₂ (a :: (l ++ [a]))

Tactic:
exact p.imp H

Premises used: List.IsChain.imp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := α → α → Prop) Chain

Tactic:
fun _a _b hab _s =>
  Chain.imp hab

Premises used: Monotone, Cycle.Chain.imp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), Membership.mem (γ := Cycle α) nil a → ∀ (b : α), Membership.mem (γ := Cycle α) nil b → r a b) →
    Chain r nil

Tactic:
fun _ ↦ Cycle.Chain.nil r

Premises used: Cycle.Chain.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ (a : α), Membership.mem (γ := Cycle α) nil a → ∀ (b : α), Membership.mem (γ := Cycle α) nil b → r a b) →
    Chain r nil

Tactic:
exact fun _ ↦ Cycle.Chain.nil r

Premises used: Cycle.Chain.nil
-- Module: Mathlib.Data.List.Cycle
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 α)
⊢ (∀ a_1 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_1 b) → Chain r (↑(a :: l) : Cycle α)

Tactic:
?_
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
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 α)
⊢ (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s

Tactic:
induction s with
  | nil => exact fun _ ↦ Cycle.Chain.nil r
  | cons a l => ?_

Premises used: Cycle.Chain.nil, List.cons, Cycle.nil
-- Module: Mathlib.Data.List.Cycle
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
⊢ a ∈ (↑(a :: l) : Cycle α)

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
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
⊢ a ∈ (↑(a :: l) : Cycle α)

Tactic:
have Ha : a ∈ (a :: l : Cycle α) := by simp
-- Module: Mathlib.Data.List.Cycle
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 α)
b : α
hb : b ∈ l
⊢ b ∈ (↑(a :: l) : Cycle α)

Tactic:
simp [hb]
-- Module: Mathlib.Data.List.Cycle
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 α)
⊢ ∀ {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]
-- Module: Mathlib.Data.List.Cycle
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 α)
cons : List.Pairwise r (a :: (l ++ [a]))
⊢ IsChain r (a :: (l ++ [a]))

Tactic:
apply Pairwise.isChain

Premises used: List.Pairwise.isChain
-- Module: Mathlib.Data.List.Cycle
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 α)
cons : (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])
⊢ List.Pairwise r (a :: (l ++ [a]))

Tactic:
rw [pairwise_cons]

Premises used: List.pairwise_cons
-- Module: Mathlib.Data.List.Cycle
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 α)
b : α
hb : b ∈ l ++ [a]
⊢ r a b

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
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 α)
b : α
hb : b ∈ l
c : α
hc : c ∈ [a]
⊢ r b c

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
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 α)
⊢ (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])

Tactic:
exact
    ⟨fun b hb => by grind,
      pairwise_append.2
        ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc),
          pairwise_singleton r a, fun b hb c hc => by grind⟩⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
⊢ Chain r nil → ∀ (a : α), Membership.mem (γ := Cycle α) nil a → ∀ (b : α), Membership.mem (γ := Cycle α) nil b → r a b

Tactic:
fun _ b hb ↦ (notMem_nil _ hb).elim

Premises used: False.elim, Cycle.notMem_nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
⊢ Chain r nil → ∀ (a : α), Membership.mem (γ := Cycle α) nil a → ∀ (b : α), Membership.mem (γ := Cycle α) nil b → r a b

Tactic:
exact fun _ b hb ↦ (notMem_nil _ hb).elim

Premises used: False.elim, Cycle.notMem_nil
-- Module: Mathlib.Data.List.Cycle
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
⊢ Chain r (↑(a :: l) : Cycle α) → ∀ a_2 ∈ (↑(a :: l) : Cycle α), ∀ b ∈ (↑(a :: l) : Cycle α), r a_2 b

Tactic:
?_
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst : IsTrans α r
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
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
induction s with
    | nil => exact fun _ b hb ↦ (notMem_nil _ hb).elim
    | cons a l => ?_

Premises used: False.elim, List.cons, Cycle.notMem_nil, Cycle.nil
-- Module: Mathlib.Data.List.Cycle
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 α)
cons :
  ∀ (hs : List.Pairwise r (a :: (l ++ [a]))) (b : α) (hb : b ∈ (↑(a :: l) : Cycle α)) (c : α)
    (hc : c ∈ (↑(a :: l) : Cycle α)), r b c
⊢ r b c

Tactic:
rw [Cycle.chain_coe_cons, List.isChain_iff_pairwise] at hs

Premises used: List.isChain_iff_pairwise, Cycle.chain_coe_cons
-- Module: Mathlib.Data.List.Cycle
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 α)
⊢ (∀ (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

Premises used: forall_eq, List.mem_singleton, List.pairwise_append, imp_true_iff, List.pairwise_cons, List.Pairwise.nil, List.mem_append, List.not_mem_nil, true_and, IsEmpty.forall_iff
-- Module: Mathlib.Data.List.Cycle
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
⊢ b = a ∨ b ∈ l

Tactic:
simp only [mem_coe_iff, mem_cons] at hb hc

Premises used: Cycle.mem_coe_iff, List.mem_cons
-- Module: Mathlib.Data.List.Cycle
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
⊢ c = a ∨ c ∈ l

Tactic:
simp only [mem_coe_iff, mem_cons] at hb hc

Premises used: Cycle.mem_coe_iff, List.mem_cons
-- Module: Mathlib.Data.List.Cycle
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
cons₁ : ∀ (hb : b ∈ l), r b c
⊢ r b c

Tactic:
rcases hb with (rfl | hb)

Premises used: rfl
-- Module: Mathlib.Data.List.Cycle
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
cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c), r c c
cons₁ : ∀ (hc : c ∈ l), r b c
⊢ r b c

Tactic:
rcases hc with (rfl | hc)

Premises used: rfl
-- Module: Mathlib.Data.List.Cycle
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
hc : c = a ∨ c ∈ l
hb : b ∈ l
cons : ∀ (hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c), r b c
cons₁ : ∀ (hc : c ∈ l), r b c
⊢ r b c

Tactic:
rcases hc with (rfl | hc)

Premises used: rfl
-- Module: Mathlib.Data.List.Cycle
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
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c

Tactic:
hs.1 c (Or.inr rfl)

Premises used: And.left, Or.inr, rfl
-- Module: Mathlib.Data.List.Cycle
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
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c

Tactic:
exact hs.1 c (Or.inr rfl)

Premises used: And.left, Or.inr, rfl
-- Module: Mathlib.Data.List.Cycle
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 ∈ l
⊢ r b c

Tactic:
hs.1 c (Or.inl hc)

Premises used: And.left, Or.inl