awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l l' : List α
nil : ∀ (l' : List α), ([] ++ l').rotate' (length.{u} (α := α) []) = l' ++ []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (l' : List α), (tail ++ l').rotate' tail.length = l' ++ tail) →
      ∀ (l' : List α), (head :: tail ++ l').rotate' (head :: tail).length = l' ++ head :: tail
⊢ (l ++ l').rotate' l.length = l' ++ l

Tactic:
induction l generalizing l'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l' : List α
⊢ ([] ++ l').rotate' (length.{u} (α := α) []) = l' ++ []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
head : α
tail : List α
tail_ih : ∀ (l' : List α), (tail ++ l').rotate' tail.length = l' ++ tail
l' : List α
⊢ (head :: tail ++ l').rotate' (head :: tail).length = l' ++ head :: tail

Tactic:
simp_all [rotate']

Premises used: List.rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
rw : (l.rotate n).rotate' m = l.rotate (n + m)
rw₁ : (l.rotate' n).rotate' m = l.rotate (n + m)
rw₂ : (l.rotate' n).rotate' m = l.rotate' (n + m)
rw₃ rw₄ : l.rotate' (n + m) = l.rotate' (n + m)
⊢ (l.rotate n).rotate m = l.rotate (n + m)

Tactic:
rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']

Premises used: List.rotate_eq_rotate', List.rotate'_rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
rw : l.rotate' l.length = l
rw₁ rw₂ : l = l
⊢ l.rotate l.length = l

Tactic:
rw [rotate_eq_rotate', rotate'_length]

Premises used: List.rotate_eq_rotate', List.rotate'_length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate' (l.length * n) = l
rw₁ rw₂ : l = l
⊢ l.rotate (l.length * n) = l

Tactic:
rw [rotate_eq_rotate', rotate'_length_mul]

Premises used: List.rotate'_length_mul, List.rotate_eq_rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate' n ~ l
⊢ l.rotate n ~ l

Tactic:
rw [rotate_eq_rotate']

Premises used: List.rotate_eq_rotate'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ l.rotate' 0 ~ l

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
succ : Perm.{u} (α := α) (rotate' [] (n + 1)) []
succ₁ : ∀ (hd : α) (tl : List α), (hd :: tl).rotate' (n + 1) ~ hd :: tl
⊢ l.rotate' (n + 1) ~ l

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ Perm.{u} (α := α) (rotate' [] (n + 1)) []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
succ : (tl ++ [hd]).rotate' n ~ hd :: tl
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
rw [rotate'_cons_succ]

Premises used: List.rotate'_cons_succ
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl

Tactic:
(hn _).trans (perm_append_singleton _ _)

Premises used: List.Perm.trans, List.perm_append_singleton
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl

Tactic:
exact (hn _).trans (perm_append_singleton _ _)

Premises used: List.Perm.trans, List.perm_append_singleton
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ (l : List α), l.rotate' 0 ~ l
succ : ∀ (n : ℕ) (hn : ∀ (l : List α), l.rotate' n ~ l) (l : List α), l.rotate' (n + 1) ~ l
⊢ l.rotate' n ~ l

Tactic:
induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

Premises used: List.rotate'_cons_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).Nodup ↔ l.Nodup

Tactic:
(rotate_perm l n).nodup_iff

Premises used: List.rotate_perm, List.Perm.nodup_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
⊢ l.rotate 0 = [] ↔ l = []

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
succ : Eq.{u + 1} (α := List α) (rotate [] (n + 1)) [] ↔ Eq.{u + 1} (α := List α) [] []
succ₁ : ∀ (hd : α) (tl : List α), (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []
⊢ l.rotate (n + 1) = [] ↔ l = []

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

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
simp [rotate_cons_succ, hn]

Premises used: List.rotate_cons_succ
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ {l : List α}, l.rotate 0 = [] ↔ l = []
succ : ∀ (n : ℕ) (hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []) {l : List α}, l.rotate (n + 1) = [] ↔ l = []
⊢ l.rotate n = [] ↔ l = []

Tactic:
induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [rotate_cons_succ, hn]

Premises used: List.rotate_cons_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
rw : l.rotate n = [] ↔ [] = l
rw₁ : l = [] ↔ [] = l
rw₂ rw₃ : [] = l ↔ [] = l
⊢ [] = l.rotate n ↔ [] = l

Tactic:
rw [eq_comm, rotate_eq_nil_iff, eq_comm]

Premises used: eq_comm, List.rotate_eq_nil_iff
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
x : α
n : ℕ
⊢ [x].rotate n = [x]

Tactic:
rotate_replicate x 1 n

Premises used: List.replicate, List.rotate_replicate, OfNat.ofNat
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
rw : (drop (n % l'.length) l).length = (drop (n % l'.length) l').length
⊢ (zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod,
    rotate_eq_drop_append_take_mod, h, zipWith_append, ← drop_zipWith, ←
    take_zipWith, List.length_zipWith, h, min_self]

Premises used: List.drop_zipWith, List.take_zipWith, List.length_zipWith, min_self, List.rotate_eq_drop_append_take_mod, List.zipWith_append
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : l.length = l'.length
rw : l.length - n % l'.length = (drop (n % l'.length) l').length
rw₁ : l.length - n % l'.length = l'.length - n % l'.length
rw₂ rw₃ : l'.length - n % l'.length = l'.length - n % l'.length
⊢ (drop (n % l'.length) l).length = (drop (n % l'.length) l').length

Tactic:
rw [length_drop, length_drop, h]

Premises used: List.length_drop
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
β : Type u_1
f : α → α → β
x y : α
l : List α
⊢ zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x])

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)

Tactic:
rw [rotate_eq_drop_append_take_mod]

Premises used: List.rotate_eq_drop_append_take_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
inl :
  ∀ (hm : m < (drop (n % l.length) l).length),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
inr :
  ∀ (hm : (drop (n % l.length) l).length ≤ m),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)

Tactic:
rcases lt_or_ge m (l.drop (n % l.length)).length with hm | hm

Premises used: HMod.hMod, List.drop, lt_or_ge, List.length
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
inl :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n % l.length) % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)

Tactic:
rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]

Premises used: List.getElem?_drop, List.getElem?_append_left, Nat.add_mod_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ m + n % l.length < l.length

Tactic:
rw [length_drop, Nat.lt_sub_iff_add_lt] at hm

Premises used: Nat.lt_sub_iff_add_lt, List.length_drop
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
inl :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length)
inl₁ inl₂ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m + n % l.length)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length + m) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n % l.length) % l.length)

Tactic:
rw [mod_eq_of_lt hm, Nat.add_comm]

Premises used: Nat.mod_eq_of_lt, Nat.add_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ n % l.length < l.length

Tactic:
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
inr :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m - (l.length - n % l.length)) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)
inr₁ : m - (drop (n % l.length) l).length < n % l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop (n % l.length) l ++ take (n % l.length) l) m =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)

Tactic:
rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]

Premises used: List.getElem?_append_right, List.length_drop, List.getElem?_take_of_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
inr : m - (l.length - n % l.length) = (m + n) % l.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (m - (l.length - n % l.length)) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((m + n) % l.length)

Tactic:
congr 1
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l.length - n % l.length ≤ m

Tactic:
rw [length_drop] at hm

Premises used: List.length_drop
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
hm₁ : l.length - n % l.length ≤ m
⊢ n % l.length < l.length

Tactic:
rw [length_drop] at hm

Premises used: List.length_drop
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
⊢ l.length ≤ n % l.length + m

Tactic:
have hm' := Nat.sub_le_iff_le_add'.1 hm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
rw : n % l.length + m < l.length + l.length
⊢ n % l.length + m - l.length < l.length

Tactic:
rw [Nat.sub_lt_iff_lt_add hm']

Premises used: Nat.sub_lt_iff_lt_add
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m < l.length + l.length

Tactic:
Nat.add_lt_add hlt hml

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m < l.length + l.length

Tactic:
exact Nat.add_lt_add hlt hml

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m - l.length < l.length

Tactic:
have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
rw : n % l.length + m - l.length
| (m + n) % l.length

Tactic:
rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]

Premises used: Nat.mod_eq_of_lt, Nat.mod_add_mod, Nat.mod_eq_sub_mod, Nat.add_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
inr : m - (l.length - n % l.length) = n % l.length + m - l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]

Premises used: Nat.mod_eq_of_lt, Nat.mod_add_mod, Nat.mod_eq_sub_mod, Nat.add_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = n % l.length + m - l.length

Tactic:
lia
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
inr : m < (drop (n % l.length) l).length + n % l.length
inr₁ : m < l.length - n % l.length + n % l.length
inr₂ inr₃ inr₄ inr₅ : m < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

Premises used: List.length_drop, LT.lt.le, Nat.sub_add_cancel, Nat.sub_lt_iff_lt_add'
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
rw : k < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) k h =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + n) % l.length) ⋯

Tactic:
rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]

Premises used: List.getElem?_rotate, List.getElem?_eq_getElem, Option.some_inj
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length

Tactic:
h.trans_eq (length_rotate _ _)

Premises used: List.length_rotate, LT.lt.trans_eq
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length

Tactic:
exact h.trans_eq (length_rotate _ _)

Premises used: List.length_rotate, LT.lt.trans_eq
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
k : Fin (l.rotate n).length
⊢ (l.rotate n).get k = l.get ⟨((↑k : ℕ) + n) % l.length, ⋯⟩

Tactic:
simp [getElem_rotate]

Premises used: List.getElem_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
rw :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) 0 =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
rw₁ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((0 + n) % l.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
rw₂ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n % l.length) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
rw₃ rw₄ :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
⊢ (l.rotate n).head? = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n

Tactic:
rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]

Premises used: List.getElem?_rotate, Nat.zero_le, List.head?_eq_getElem?, Nat.mod_eq_of_lt, Nat.zero_add, LE.le.trans_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
k : Fin (l.rotate 1).length
⊢ (l.rotate 1).get k = l.get ⟨((↑k : ℕ) + 1) % l.length, ⋯⟩

Tactic:
get_rotate l 1 k

Premises used: List.get_rotate, OfNat.ofNat
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l
      (((l.length - n % l.length + k) % l.length + n) % l.length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n) ((l.length - n % l.length + k) % l.length)
      ⋯

Tactic:
rw [getElem_rotate]

Premises used: List.getElem_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l
      (((l.length - n % l.length + k) % l.length + n) % l.length) ⋯

Tactic:
congr_arg l.get (Fin.eq_of_val_eq ?_)

Premises used: List.get, Fin.eq_of_val_eq, congr_arg
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
refine : (↑(⟨k, hk⟩ : Fin l.length) : ℕ) = (↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, ⋯⟩ : ℕ)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l
      (((l.length - n % l.length + k) % l.length + n) % l.length) ⋯

Tactic:
refine congr_arg l.get (Fin.eq_of_val_eq ?_)

Premises used: List.get, Fin.eq_of_val_eq, congr_arg
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
simp : k = (l.length - n % l.length + k + n) % l.length
⊢ (↑(⟨k, hk⟩ : Fin l.length) : ℕ) = (↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, ⋯⟩ : ℕ)

Tactic:
simp only [mod_add_mod]

Premises used: Nat.mod_add_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk rw : k < l.length
rw₁ : n % l.length ≤ l.length
⊢ k = (l.length - n % l.length + k + n) % l.length

Tactic:
rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]

Premises used: Nat.add_mod_mod, Nat.mod_eq_of_lt, Nat.sub_add_cancel, Nat.add_mod_left, Nat.add_right_comm
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

Tactic:
hk
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length

Tactic:
(mod_lt _ (k.zero_le.trans_lt hk)).le

Premises used: Nat.zero_le, LT.lt.le, Nat.mod_lt, LE.le.trans_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

Tactic:
exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]

Premises used: Nat.zero_le, LT.lt.le, Nat.mod_lt, LE.le.trans_lt
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
l : List α
n : ℕ
k : Fin l.length
⊢ l.get k = (l.rotate n).get (⟨(l.length - n % l.length + (↑k : ℕ)) % l.length, ⋯⟩ : Fin (l.rotate n).length)

Tactic:
simpa using getElem_eq_getElem_rotate _ _ _ _

Premises used: List.getElem_eq_getElem_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hα : Nonempty α
⊢ (∀ (n : ℕ), Eq.{u + 1} (α := List α) (rotate [] n) []) ↔ ∃ (a : α), [] = replicate (length.{u} (α := α) []) a

Tactic:
simp
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n h₁ = a
rw₁ : some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n h₁) = some a
rw₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n = some a
rw₃ : ((a :: l).rotate n).head? = some a
rw₄ : (a :: l).head? = some a
rw₅ rw₆ : some a = some a
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (replicate (a :: l).length a) n h₂

Tactic:
rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]

Premises used: List.getElem_replicate, List.getElem?_eq_getElem, List.head?_cons, List.head?_rotate, Option.some_inj
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∃ (a_1 : α), a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
rw : (replicate (a :: l).length b).rotate n = replicate (a :: l).length b
rw₁ rw₂ : replicate (a :: l).length b = replicate (a :: l).length b
⊢ (a :: l).rotate n = a :: l

Tactic:
rw [hb, rotate_replicate]

Premises used: List.rotate_replicate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
inst : Nonempty α
l : List α
h : l.rotate 1 = l
n_1 n : ℕ
hn : l.rotate n = l
rwa : l.rotate (n + 1) = l
rwa₁ : (l.rotate n).rotate 1 = l
rwa₂ rwa₃ rwa₄ rwa₅ : l.rotate 1 = l
⊢ l.rotate n.succ = l

Tactic:
rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]

Premises used: Nat.succ_eq_add_one, List.rotate_rotate
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
⊢ l.length = l'.length

Tactic:
have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
⊢ drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h

Premises used: List.rotate_eq_drop_append_take_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
h₁ : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
⊢ l.length = l'.length

Tactic:
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h

Premises used: List.rotate_eq_drop_append_take_mod
-- Module: Mathlib.Data.List.Rotate
Goal:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
⊢ (drop (n % l.length) l).length = (drop (n % l'.length) l').length

Tactic:
simp_all