awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l = l.reverse.reverse

Tactic:
(reverse_reverse l).symm

Premises used: List.reverse_reverse, Eq.symm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l = l.reverse.reverse

Tactic:
exact (reverse_reverse l).symm

Premises used: List.reverse_reverse, Eq.symm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
obtain :
  ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
      l'.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯
⊢ l.next x hx = l'.next x ⋯

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
obtain :
  ∀ (n : ℕ) (h : l ~r l.rotate n),
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
      (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯
⊢ l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
    l'.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯

Tactic:
obtain ⟨n, rfl⟩ := id h

Premises used: id, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯
⊢ l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
    (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯

Tactic:
rw [next_getElem _ hn]

Premises used: List.next_getElem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
simp_rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    (l.rotate n).next
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
        ((l.length - n % l.length + k) % l.length) ⋯)
      ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯

Tactic:
simp_rw [getElem_eq_getElem_rotate _ n k]

Premises used: List.getElem_eq_getElem_rotate
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
      ((l.length - n % l.length + (k + 1) % l.length) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
      (((l.length - n % l.length + k) % l.length + 1) % (l.rotate n).length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    (l.rotate n).next
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
        ((l.length - n % l.length + k) % l.length) ⋯)
      ⋯

Tactic:
rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]

Premises used: List.IsRotated.nodup_iff, Iff.mp, List.next_getElem, List.getElem_eq_getElem_rotate
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
      ((l.length - n % l.length + (k + 1) % l.length) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
      (((l.length - n % l.length + k) % l.length + 1) % (l.rotate n).length) ⋯

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
rw : l.reverse.next x ⋯ = l'.reverse.next x ⋯
⊢ l.prev x hx = l'.prev x ⋯

Tactic:
rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]

Premises used: List.next_reverse_eq_prev, List.IsRotated.nodup_iff, Iff.mp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.reverse.next x ⋯

Tactic:
isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

Premises used: Iff.mpr, List.IsRotated.reverse, List.nodup_reverse, List.isRotated_next_eq
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.reverse.next x ⋯

Tactic:
exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

Premises used: Iff.mpr, List.IsRotated.reverse, List.nodup_reverse, List.isRotated_next_eq
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ (↑l₁ : Cycle α) = (↑l₂ : Cycle α) ↔ l₁ ~r l₂

Tactic:
@Quotient.eq _ (IsRotated.setoid _) _ _

Premises used: Cycle.ofList, Quotient.eq, Cycle
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l = (↑l : Cycle α)

Tactic:
rfl

Premises used: Cycle.ofList, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ Quotient.mk'' l = (↑l : Cycle α)

Tactic:
rfl

Premises used: Cycle.ofList, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
a : α
rw : (l ++ [a]).rotate 0 = l ++ [a]
rw₁ rw₂ : l ++ [a] = l ++ [a]
⊢ (a :: l).rotate 1 = l ++ [a]

Tactic:
rw [rotate_cons_succ, rotate_zero]

Premises used: List.rotate_cons_succ, List.rotate_zero
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Cycle α) (↑[] : Cycle α) nil

Tactic:
rfl

Premises used: rfl, Cycle.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ (↑l : Cycle α) = nil ↔ l = []

Tactic:
coe_eq_coe.trans isRotated_nil_iff

Premises used: Cycle.coe_eq_coe, List.isRotated_nil_iff, Iff.trans, Cycle.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Cycle α) ∅ nil

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive (↑l : Cycle α) → motive (↑(a :: l) : Cycle α)
l : List α
⊢ motive (Quotient.mk'' l)

Tactic:
List.recOn l ?_ ?_

Premises used: List.recOn
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive (↑l : Cycle α) → motive (↑(a :: l) : Cycle α)
l : List α
refine_1 : motive (Quotient.mk'' [])
refine_2 : ∀ (head : α) (tail : List α) (tail_ih : motive (Quotient.mk'' tail)), motive (Quotient.mk'' (head :: tail))
⊢ motive (Quotient.mk'' l)

Tactic:
refine List.recOn l ?_ ?_
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive (↑l : Cycle α) → motive (↑(a :: l) : Cycle α)
l : List α
refine_1 : motive Cycle.nil
⊢ motive (Quotient.mk'' [])

Tactic:
simp only [mk''_eq_coe, coe_nil]

Premises used: Cycle.coe_nil, Cycle.mk''_eq_coe
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive (↑l : Cycle α) → motive (↑(a :: l) : Cycle α)
l : List α
refine_2 : ∀ (head : α) (tail : List α) (tail_ih : motive (↑tail : Cycle α)), motive (↑(head :: tail) : Cycle α)
⊢ ∀ (head : α) (tail : List α) (tail_ih : motive (Quotient.mk'' tail)), motive (Quotient.mk'' (head :: tail))

Tactic:
simp only [mk''_eq_coe, coe_nil]

Premises used: Cycle.coe_nil, Cycle.mk''_eq_coe
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
a : α
l : List α
⊢ a ∈ (↑l : Cycle α) ↔ a ∈ l

Tactic:
Iff.rfl

Premises used: Iff.rfl, Cycle.Mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
a : α
⊢ a ∉ nil

Tactic:
List.not_mem_nil

Premises used: Cycle.Mem, List.not_mem_nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ (↑l : Cycle α).reverse = (↑l.reverse : Cycle α)

Tactic:
rfl

Premises used: Cycle.ofList, Quot.map, Cycle.reverse, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
a : α
s : Cycle α
⊢ a ∈ s.reverse ↔ a ∈ s

Tactic:
Quot.inductionOn s fun _ => mem_reverse

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
x : List α
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) x)).reverse =
    Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) x

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Cycle α) (reverse nil) nil

Tactic:
rfl

Premises used: List.reverseAux, Cycle.ofList, Quot.map, List.reverse, rfl, Cycle.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ (↑l : Cycle α).length = l.length

Tactic:
rfl

Premises used: Cycle.length, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ length.{u_1} (α := α) nil = 0

Tactic:
rfl

Premises used: Cycle.length, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ s.reverse.length = s.length

Tactic:
Quot.inductionOn s fun _ => List.length_reverse

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Subsingleton.{u_1} (α := α) nil

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le, Cycle.Subsingleton, Cycle.length
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ s.Subsingleton ↔ s.length ≤ 1

Tactic:
Iff.rfl

Premises used: Iff.rfl, Cycle.Subsingleton
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ s.reverse.Subsingleton ↔ s.Subsingleton

Tactic:
simp [length_subsingleton_iff]

Premises used: Cycle.length_subsingleton_iff
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
h : s.Subsingleton
h₁ :
  ∀ (l : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) ⦃x : α⦄
    (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ⦃y : α⦄
    (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y), x = y
⊢ ∀ ⦃x : α⦄ (_hx : x ∈ s) ⦃y : α⦄ (_hy : y ∈ s), x = y

Tactic:
induction s using Quot.inductionOn with | _ l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
⊢ l = [] ∨ ∃ (a : α), l = [a]

Tactic:
simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
    length_eq_zero_iff, length_eq_one_iff, Nat.not_lt_zero, false_or] at h

Premises used: Cycle.mk_eq_coe, Nat.lt_add_one_iff, false_or, List.length_eq_one_iff, Cycle.length_subsingleton_iff, Cycle.length_coe, le_iff_lt_or_eq, Nat.not_lt_zero, List.length_eq_zero_iff
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
h : l = [] ∨ ∃ (a : α), l = [a]
h₁ :
  ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
    ⦃y : α⦄ (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y), x = y
h₂ :
  ∀ (z : α) ⦃x : α⦄
    (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [z]) x) ⦃y : α⦄
    (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [z]) y), x = y
⊢ ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ⦃y : α⦄
    (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y), x = y

Tactic:
rcases h with (rfl | ⟨z, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
    ⦃y : α⦄ (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y), x = y

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
z : α
⊢ ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [z]) x)
    ⦃y : α⦄ (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [z]) y),
    x = y

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
hl : l.Nodup
nil :
  ∀ (hl : Nodup.{u_1} (α := α) []),
    (∃ (x : α) (y : α),
        x ≠ y ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) x ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) y) ↔
      2 ≤ List.length.{u_1} (α := α) []
cons :
  ∀ (hd : α) (hl : [hd].Nodup),
    (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑[hd] : Cycle α) ∧ y ∈ (↑[hd] : Cycle α)) ↔ 2 ≤ [hd].length
cons₁ :
  ∀ (hd hd' : α) (tl : List α) (hl : (hd :: hd' :: tl).Nodup),
    (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑(hd :: hd' :: tl) : Cycle α) ∧ y ∈ (↑(hd :: hd' :: tl) : Cycle α)) ↔
      2 ≤ (hd :: hd' :: tl).length
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑l : Cycle α) ∧ y ∈ (↑l : Cycle α)) ↔ 2 ≤ l.length

Tactic:
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hl : Nodup.{u_1} (α := α) []
⊢ (∃ (x : α) (y : α),
      x ≠ y ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) x ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) y) ↔
    2 ≤ List.length.{u_1} (α := α) []

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑[hd] : Cycle α) ∧ y ∈ (↑[hd] : Cycle α)) ↔ 2 ≤ [hd].length

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
cons : ∃ (x : α) (y : α), ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑(hd :: hd' :: tl) : Cycle α) ∧ y ∈ (↑(hd :: hd' :: tl) : Cycle α)) ↔
    2 ≤ (hd :: hd' :: tl).length

Tactic:
simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]

Premises used: Cycle.mem_coe_iff, Nat.zero_le, iff_true, Ne, Nat.succ_le_succ_iff, List.mem_cons, List.length
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
cons : ¬hd = hd'
⊢ ∃ (x : α) (y : α), ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)

Tactic:
refine ⟨hd, hd', ?_, by simp⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup

Tactic:
simp only [not_or, mem_cons, nodup_cons] at hl

Premises used: not_or, List.nodup_cons, List.mem_cons
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup
⊢ ¬hd = hd'

Tactic:
hl.left.left

Premises used: And.left
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup
⊢ ¬hd = hd'

Tactic:
exact hl.left.left

Premises used: And.left
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ s.reverse.Nontrivial ↔ s.Nontrivial

Tactic:
simp [Nontrivial]

Premises used: Cycle.Nontrivial
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
h : s.Nontrivial
obtain : ∀ (x y : α) (hxy : x ≠ y) (hx : x ∈ s) (hy : y ∈ s), 2 ≤ s.length
⊢ 2 ≤ s.length

Tactic:
obtain ⟨x, y, hxy, hx, hy⟩ := h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
h :
  ∀ (l : List α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y),
    2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
⊢ 2 ≤ s.length

Tactic:
induction s using Quot.inductionOn with | _ l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y
h :
  ∀ (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y),
    2 ≤ length.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
h₁ :
  ∀ (hd : α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y),
    2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd])
h₂ :
  ∀ (hd hd' : α) (tl : List α)
    (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl)) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl)) y),
    2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl))
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)

Tactic:
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y
⊢ 2 ≤ length.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])

Tactic:
simp at hx
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y
⊢ x = hd

Tactic:
simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy

Premises used: Cycle.mem_coe_iff, Cycle.mk_eq_coe, List.mem_singleton
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y
hx₁ : x = hd
⊢ y = hd

Tactic:
simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy

Premises used: Cycle.mem_coe_iff, Cycle.mk_eq_coe, List.mem_singleton
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd])

Tactic:
simp [hx, hy] at hxy
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl)) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl)) y
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl))

Tactic:
simp [Nat.succ_le_succ_iff]

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Nodup.{u_1} (α := α) nil

Tactic:
nodup_nil

Premises used: List.nodup_nil, Cycle.Nodup
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ (↑l : Cycle α).Nodup ↔ l.Nodup

Tactic:
Iff.rfl

Premises used: Iff.rfl, Cycle.Nodup
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ s.reverse.Nodup ↔ s.Nodup

Tactic:
Quot.inductionOn s fun _ => nodup_reverse

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
h : s.Subsingleton
h₁ :
  ∀ (l : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)),
    Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
⊢ s.Nodup

Tactic:
induction s using Quot.inductionOn with | _ l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
h₁ :
  ∀ (h : Subsingleton.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])),
    Nodup.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
h₂ :
  ∀ (hd : α) (tl : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))),
    Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)

Tactic:
obtain - | ⟨hd, tl⟩ := l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
h : Subsingleton.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
⊢ Nodup.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
⊢ tl = []

Tactic:
simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h

Premises used: Cycle.Subsingleton, Nat.succ_le_succ_iff, List.length_eq_zero_iff
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
⊢ tl = []

Tactic:
have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
this : tl = []
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))

Tactic:
simp [this]
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
h : s.Nodup
h₁ : ∀ (a : List α) (h : Nodup (Quotient.mk'' a)), Nontrivial (Quotient.mk'' a) ↔ ¬length (Quotient.mk'' a) ≤ 1
⊢ s.Nontrivial ↔ ¬s.length ≤ 1

Tactic:
induction s using Quotient.inductionOn'
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
a : List α
h : Nodup (Quotient.mk'' a)
⊢ a.Nodup

Tactic:
simp only [mk''_eq_coe, nodup_coe_iff] at h

Premises used: Cycle.nodup_coe_iff, Cycle.mk''_eq_coe
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
a : List α
h : a.Nodup
⊢ Nontrivial (Quotient.mk'' a) ↔ ¬length (Quotient.mk'' a) ≤ 1

Tactic:
simp [h, Nat.succ_le_iff]

Premises used: Nat.succ_le_iff
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ (↑l : Cycle α).toMultiset = (↑l : Multiset α)

Tactic:
rfl

Premises used: Cycle.toMultiset, Multiset.ofList, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) (toMultiset nil) 0

Tactic:
rfl

Premises used: Cycle.toMultiset, Quotient.liftOn', Multiset.zero, Multiset.ofList, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), (toMultiset (Quotient.mk'' a)).card = length (Quotient.mk'' a)

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), toMultiset (Quotient.mk'' a) = 0 ↔ Quotient.mk'' a = nil

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f nil = nil

Tactic:
rfl

Premises used: List.map, Cycle.ofList, Quot.map, Quotient.map', rfl, Cycle.nil