awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
refine : ∀ (h : l ~r l'), ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'
⊢ l ~r l' ↔ ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'

Tactic:
refine ⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l ~r l'
obtain : ∀ (n : ℕ), ∃ (n_1 : ℕ), n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n
⊢ ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
nil : ∃ (n_1 : ℕ), n_1 ≤ length.{u} (α := α) [] ∧ Eq.{u + 1} (α := List α) (rotate [] n_1) (rotate [] n)
cons : ∀ (hd : α) (tl : List α), ∃ (n_1 : ℕ), n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n
⊢ ∃ (n_1 : ℕ), n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
⊢ ∃ (n_1 : ℕ), n_1 ≤ length.{u} (α := α) [] ∧ Eq.{u + 1} (α := List α) (rotate [] n_1) (rotate [] n)

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ (n_1 : ℕ), n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Tactic:
⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩

Premises used: List.rotate_mod, List.cons, HMod.hMod, And.intro, Exists.intro, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
cons : n % (hd :: tl).length ≤ (hd :: tl).length
⊢ ∃ (n_1 : ℕ), n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Tactic:
refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % (hd :: tl).length ≤ (hd :: tl).length

Tactic:
(Nat.mod_lt _ ?_).le

Premises used: LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
cons : 0 < (hd :: tl).length
⊢ n % (hd :: tl).length ≤ (hd :: tl).length

Tactic:
refine (Nat.mod_lt _ ?_).le

Premises used: LT.lt.le, Nat.mod_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
simp_rw : (∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l') ↔ ∃ (a : ℕ), a < l.length + 1 ∧ l.rotate a = l'
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))

Tactic:
simp_rw [mem_map, mem_range, isRotated_iff_mod]

Premises used: List.mem_range, List.isRotated_iff_mod, List.mem_map
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ (∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l') ↔ ∃ (a : ℕ), a < l.length + 1 ∧ l.rotate a = l'

Tactic:
⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩,
      fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩

Premises used: Exists, Nat.lt_succ_of_le, LE.le, And, HAdd.hAdd, Nat.le_of_lt_succ, And.intro, LT.lt, Iff.intro, _private.0.List.isRotated_iff_mem_map_range.match_3, Exists.intro, OfNat.ofNat, Eq, List.length, _private.0.List.isRotated_iff_mod.match_1, List.rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ (∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l') ↔ ∃ (a : ℕ), a < l.length + 1 ∧ l.rotate a = l'

Tactic:
exact
    ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩,
      fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
obtain : ∀ (n : ℕ), List.map f l₁ ~r List.map f (l₁.rotate n)
⊢ List.map f l₁ ~r List.map f l₂

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
rw : List.map f l₁ ~r (List.map f l₁).rotate n
⊢ List.map f l₁ ~r List.map f (l₁.rotate n)

Tactic:
rw [map_rotate]

Premises used: List.map_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n w : ℕ
h : (List.map f l₁).rotate n = (List.map f l₁).rotate n
⊢ List.map f l₁ ~r (List.map f l₁).rotate n

Tactic:
use n
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
a : α
⊢ a :: l ~r l ++ [a]

Tactic:
simpa using isRotated_append (l := [a])

Premises used: List.isRotated_append
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hL : Ne.{u + 1} (α := List α) [] []
⊢ getLast [] hL :: dropLast [] ~r []

Tactic:
simp at hL
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : List α
L : α
h : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
append_singleton : (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]
⊢ (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]

Tactic:
simp only [getLast_append, dropLast_concat]

Premises used: List.getLast_append, List.dropLast_concat
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : List α
L : α
h : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
append_singleton : a ++ [L] ~r (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a
⊢ (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]

Tactic:
apply IsRotated.symm

Premises used: List.IsRotated.symm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : List α
L : α
h : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ a ++ [L] ~r (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a

Tactic:
apply isRotated_concat

Premises used: List.isRotated_concat
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
L : List α
hL : L ≠ []
nil : ∀ (hL : Ne.{u + 1} (α := List α) [] []), getLast [] hL :: dropLast [] ~r []
append_singleton :
  ∀ (a : List α) (L : α),
    (∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a) →
      ∀ (hL : a ++ [L] ≠ []), (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]
⊢ L.getLast hL :: L.dropLast ~r L

Tactic:
induction L using List.reverseRecOn with
  | nil => simp at hL
  | append_singleton a L _ =>
    simp only [getLast_append, dropLast_concat]
    apply IsRotated.symm
    apply isRotated_concat

Premises used: List.isRotated_concat, List.getLast_append, List.IsRotated.symm, List.dropLast_concat, List.nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u_1
L : List α
hL : Ne.{u_1 + 1} (α := List α) [] []
hL' : head [] hL = getLast [] hL
⊢ IsRotated.{u_1} (α := α) (dropLast []) (tail [])

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u_1
L : List α
head : α
hL : [head] ≠ []
hL' : [head].head hL = [head].getLast hL
⊢ [head].dropLast ~r [head].tail

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u_1
L_1 : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : (a :: b :: L).head hL = (a :: b :: L).getLast hL
⊢ a = (b :: L).getLast ⋯

Tactic:
simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'

Premises used: reduceCtorEq, List.head_cons, ne_eq, List.getLast_cons, not_false_eq_true
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u_1
L_1 : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : a = (b :: L).getLast ⋯
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
simp [hL', IsRotated.cons_getLast_dropLast]

Premises used: List.IsRotated.cons_getLast_dropLast
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List (List α)) (cyclicPermutations []) [[]]

Tactic:
rfl

Premises used: List.cyclicPermutations, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
x : α
l : List α
⊢ (x :: l).cyclicPermutations = dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) (x :: l).tails (x :: l).inits)

Tactic:
rfl

Premises used: List.cyclicPermutations, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
h : l ≠ []
obtain :
  ∀ (hd : α) (tl : List α) (h : hd :: tl ≠ []),
    (hd :: tl).cyclicPermutations =
      dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) (hd :: tl).tails (hd :: tl).inits)
⊢ l.cyclicPermutations = dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) l.tails l.inits)

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h

Premises used: List.exists_cons_of_ne_nil, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ (hd :: tl).cyclicPermutations = dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) (hd :: tl).tails (hd :: tl).inits)

Tactic:
cyclicPermutations_cons _ _

Premises used: List.cyclicPermutations_cons
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ (hd :: tl).cyclicPermutations = dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) (hd :: tl).tails (hd :: tl).inits)

Tactic:
exact cyclicPermutations_cons _ _

Premises used: List.cyclicPermutations_cons
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
x : α
l : List α
⊢ (x :: l).cyclicPermutations.length = l.length + 1

Tactic:
simp [cyclicPermutations_cons]

Premises used: List.cyclicPermutations_cons
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations.length = l.length

Tactic:
simp [cyclicPermutations_of_ne_nil _ h]

Premises used: List.cyclicPermutations_of_ne_nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
a : α
l : List α
h : (a :: l).cyclicPermutations = []
⊢ False

Tactic:
simpa using congr_arg length h

Premises used: congr_arg, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
h : n < length.{u} (α := List α) (cyclicPermutations [])
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (cyclicPermutations []) n h = rotate [] n

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
cons : drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).cyclicPermutations n h =
    (a :: l).rotate n

Tactic:
simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]

Premises used: List.getElem_tails, List.getElem_dropLast, List.cyclicPermutations_cons, List.getElem_zipWith, List.getElem_inits
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ (a :: l).length

Tactic:
simpa using h.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
cons cons₁ : drop n (a :: l) ++ take n (a :: l) = drop n (a :: l) ++ take n (a :: l)
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n

Tactic:
rw [rotate_eq_drop_append_take (by simpa using h.le)]

Premises used: List.rotate_eq_drop_append_take
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.cyclicPermutations.length
nil :
  ∀ (h : n < length.{u} (α := List α) (cyclicPermutations [])),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (cyclicPermutations []) n h = rotate [] n
cons :
  ∀ (a : α) (l : List α) (h : n < (a :: l).cyclicPermutations.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).cyclicPermutations n h =
      (a :: l).rotate n
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.cyclicPermutations n h = l.rotate n

Tactic:
cases l with
  | nil => simp
  | cons a l =>
    simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]
    rw [rotate_eq_drop_append_take (by simpa using h.le)]

Premises used: List.getElem_tails, List.getElem_dropLast, List.cons, List.rotate_eq_drop_append_take, List.cyclicPermutations_cons, List.getElem_zipWith, List.getElem_inits, List.nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : Fin l.cyclicPermutations.length
⊢ l.cyclicPermutations.get n = l.rotate (↑n : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ 0 < l.cyclicPermutations.length

Tactic:
have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
rw : l.cyclicPermutations.get (⟨0, h⟩ : Fin l.cyclicPermutations.length) = l
rw₁ : l.rotate (↑(⟨0, h⟩ : Fin l.cyclicPermutations.length) : ℕ) = l
rw₂ : l.rotate 0 = l
rw₃ rw₄ : l = l
⊢ l.cyclicPermutations.head ⋯ = l

Tactic:
rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]

Premises used: List.get_cyclicPermutations, Fin.val_mk, List.get_mk_zero, List.rotate_zero
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
rw : some (l.cyclicPermutations.head ⋯) = some l
rw₁ rw₂ : some l = some l
⊢ l.cyclicPermutations.head? = some l

Tactic:
rw [head?_eq_some_head (cyclicPermutations_ne_nil l), head_cyclicPermutations]

Premises used: List.head?_eq_some_head, List.head_cyclicPermutations, List.cyclicPermutations_ne_nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
h : l.cyclicPermutations = l'.cyclicPermutations
⊢ l = l'

Tactic:
simpa using congr_arg head? h

Premises used: List.head?, congr_arg
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
⊢ l.cyclicPermutations = l'.cyclicPermutations ↔ l = l'

Tactic:
cyclicPermutations_injective.eq_iff

Premises used: Function.Injective.eq_iff, List.cyclicPermutations_injective
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l' l : List α
h : l' ∈ l.cyclicPermutations
obtain :
  ∀ (k : Fin l.cyclicPermutations.length) (h : l.cyclicPermutations.get k ∈ l.cyclicPermutations),
    (l.cyclicPermutations.get k).length = l.length
⊢ l'.length = l.length

Tactic:
obtain ⟨k, hk, rfl⟩ := get_of_mem h

Premises used: List.get_of_mem, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : Fin l.cyclicPermutations.length
h : l.cyclicPermutations.get k ∈ l.cyclicPermutations
⊢ (l.cyclicPermutations.get k).length = l.length

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations

Tactic:
simpa using head_mem (cyclicPermutations_ne_nil l)

Premises used: List.head_mem, List.cyclicPermutations_ne_nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
nil :
  length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
    length.{u} (α := List α) (rotate (cyclicPermutations []) k)
cons :
  ∀ (head : α) (tail : List α),
    ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length

Tactic:
cases l
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
k : ℕ
⊢ length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
    length.{u} (α := List α) (rotate (cyclicPermutations []) k)

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
k : ℕ
head : α
tail : List α
cons : ((head :: tail).rotate k).length = ((head :: tail).cyclicPermutations.rotate k).length
cons₁ : (head :: tail).rotate k ≠ []
⊢ ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length

Tactic:
rw [length_cyclicPermutations_of_ne_nil]

Premises used: List.length_cyclicPermutations_of_ne_nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
k : ℕ
head : α
tail : List α
⊢ ((head :: tail).rotate k).length = ((head :: tail).cyclicPermutations.rotate k).length

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
k : ℕ
head : α
tail : List α
⊢ (head :: tail).rotate k ≠ []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length

Tactic:
have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) := by
    cases l
    · simp
    · rw [length_cyclicPermutations_of_ne_nil] <;> simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Tactic:
ext_get this fun n hn hn' => ?_

Premises used: List.ext_get
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
refine :
  ∀ (n : ℕ) (hn : n < (l.rotate k).cyclicPermutations.length) (hn' : n < (l.cyclicPermutations.rotate k).length),
    (l.rotate k).cyclicPermutations.get (⟨n, hn⟩ : Fin (l.rotate k).cyclicPermutations.length) =
      (l.cyclicPermutations.rotate k).get (⟨n, hn'⟩ : Fin (l.cyclicPermutations.rotate k).length)
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Tactic:
refine ext_get this fun n hn hn' => ?_

Premises used: List.ext_get
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
rw :
  l.rotate (((↑(⟨n, hn⟩ : Fin (l.rotate k).cyclicPermutations.length) : ℕ) + k) % l.length) =
    l.cyclicPermutations.get
      ⟨((↑(⟨n, hn'⟩ : Fin (l.cyclicPermutations.rotate k).length) : ℕ) + k) % l.cyclicPermutations.length, ⋯⟩
⊢ (l.rotate k).cyclicPermutations.get (⟨n, hn⟩ : Fin (l.rotate k).cyclicPermutations.length) =
    (l.cyclicPermutations.rotate k).get (⟨n, hn'⟩ : Fin (l.cyclicPermutations.rotate k).length)

Tactic:
rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]

Premises used: List.get_cyclicPermutations, List.rotate_rotate, List.rotate_mod, List.get_rotate, Nat.add_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
nil :
  ∀
    (this :
      length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
        length.{u} (α := List α) (rotate (cyclicPermutations []) k))
    (hn : n < length.{u} (α := List α) (cyclicPermutations (rotate [] k)))
    (hn' : n < length.{u} (α := List α) (rotate (cyclicPermutations []) k)),
    Eq.{u + 1} (α := List α)
      (rotate []
        (((↑(⟨n, hn⟩ : Fin (length.{u} (α := List α) (cyclicPermutations (rotate [] k)))) : ℕ) + k) %
          length.{u} (α := α) []))
      (get (cyclicPermutations [])
        ⟨((↑(⟨n, hn'⟩ : Fin (length.{u} (α := List α) (rotate (cyclicPermutations []) k))) : ℕ) + k) %
            length.{u} (α := List α) (cyclicPermutations []),
          ⋯⟩)
cons :
  ∀ (head : α) (tail : List α)
    (this : ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length)
    (hn : n < ((head :: tail).rotate k).cyclicPermutations.length)
    (hn' : n < ((head :: tail).cyclicPermutations.rotate k).length),
    (head :: tail).rotate
        (((↑(⟨n, hn⟩ : Fin ((head :: tail).rotate k).cyclicPermutations.length) : ℕ) + k) % (head :: tail).length) =
      (head :: tail).cyclicPermutations.get
        ⟨((↑(⟨n, hn'⟩ : Fin ((head :: tail).cyclicPermutations.rotate k).length) : ℕ) + k) %
            (head :: tail).cyclicPermutations.length,
          ⋯⟩
⊢ l.rotate (((↑(⟨n, hn⟩ : Fin (l.rotate k).cyclicPermutations.length) : ℕ) + k) % l.length) =
    l.cyclicPermutations.get
      ⟨((↑(⟨n, hn'⟩ : Fin (l.cyclicPermutations.rotate k).length) : ℕ) + k) % l.cyclicPermutations.length, ⋯⟩

Tactic:
cases l
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
k n : ℕ
this :
  length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
    length.{u} (α := List α) (rotate (cyclicPermutations []) k)
hn : n < length.{u} (α := List α) (cyclicPermutations (rotate [] k))
hn' : n < length.{u} (α := List α) (rotate (cyclicPermutations []) k)
⊢ Eq.{u + 1} (α := List α)
    (rotate []
      (((↑(⟨n, hn⟩ : Fin (length.{u} (α := List α) (cyclicPermutations (rotate [] k)))) : ℕ) + k) %
        length.{u} (α := α) []))
    (get (cyclicPermutations [])
      ⟨((↑(⟨n, hn'⟩ : Fin (length.{u} (α := List α) (rotate (cyclicPermutations []) k))) : ℕ) + k) %
          length.{u} (α := List α) (cyclicPermutations []),
        ⋯⟩)

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
k n : ℕ
head : α
tail : List α
this : ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length
hn : n < ((head :: tail).rotate k).cyclicPermutations.length
hn' : n < ((head :: tail).cyclicPermutations.rotate k).length
⊢ (head :: tail).rotate
      (((↑(⟨n, hn⟩ : Fin ((head :: tail).rotate k).cyclicPermutations.length) : ℕ) + k) % (head :: tail).length) =
    (head :: tail).cyclicPermutations.get
      ⟨((↑(⟨n, hn'⟩ : Fin ((head :: tail).cyclicPermutations.rotate k).length) : ℕ) + k) %
          (head :: tail).cyclicPermutations.length,
        ⋯⟩

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
mp : l ∈ l'.cyclicPermutations → l ~r l'
mpr : l ~r l' → l ∈ l'.cyclicPermutations
⊢ l ∈ l'.cyclicPermutations ↔ l ~r l'

Tactic:
constructor
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
mp : (∃ (n : Fin l'.cyclicPermutations.length), l'.rotate (↑n : ℕ) = l) → l ~r l'
⊢ l ∈ l'.cyclicPermutations → l ~r l'

Tactic:
simp_rw [mem_iff_get, get_cyclicPermutations]

Premises used: List.get_cyclicPermutations, List.mem_iff_get
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l' : List α
k : Fin l'.cyclicPermutations.length
⊢ l'.rotate (↑k : ℕ) ~r l'

Tactic:
.forall _ _

Premises used: List.IsRotated.forall
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l' : List α
k : Fin l'.cyclicPermutations.length
⊢ l'.rotate (↑k : ℕ) ~r l'

Tactic:
exact .forall _ _
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
mpr : l ∈ l.cyclicPermutations
⊢ l ∈ (l.rotate k).cyclicPermutations

Tactic:
rw [cyclicPermutations_rotate, mem_rotate]

Premises used: List.mem_rotate, List.cyclicPermutations_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations

Tactic:
apply mem_cyclicPermutations_self

Premises used: List.mem_cyclicPermutations_self
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ l.cyclicPermutations = [[]] ↔ l = []

Tactic:
cyclicPermutations_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', List.cyclicPermutations_injective, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
x : α
⊢ l.cyclicPermutations = [[x]] ↔ l = [x]

Tactic:
cyclicPermutations_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', List.cyclicPermutations_injective, rfl
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hn : l.Nodup
inl : ∀ (hn : Nodup.{u} (α := α) []), Nodup.{u} (α := List α) (cyclicPermutations [])
inr : ∀ (hl : l ≠ []), l.cyclicPermutations.Nodup
⊢ l.cyclicPermutations.Nodup

Tactic:
rcases eq_or_ne l [] with rfl | hl

Premises used: eq_or_ne, rfl, List.nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hn : Nodup.{u} (α := α) []
⊢ Nodup.{u} (α := List α) (cyclicPermutations [])

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
inr : Injective l.cyclicPermutations.get
⊢ l.cyclicPermutations.Nodup

Tactic:
rw [nodup_iff_injective_get]

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h :
  l.cyclicPermutations.get (⟨i, hi⟩ : Fin l.cyclicPermutations.length) =
    l.cyclicPermutations.get (⟨j, hj⟩ : Fin l.cyclicPermutations.length)
⊢ i < l.length

Tactic:
simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj

Premises used: List.length_cyclicPermutations_of_ne_nil
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h :
  l.cyclicPermutations.get (⟨i, hi⟩ : Fin l.cyclicPermutations.length) =
    l.cyclicPermutations.get (⟨j, hj⟩ : Fin l.cyclicPermutations.length)
hi₁ : i < l.length
⊢ j < l.length

Tactic:
simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj

Premises used: List.length_cyclicPermutations_of_ne_nil