awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ (↑(⟨k, hk⟩ : Fin l.length) : ℕ) = (↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, ⋯⟩ : ℕ)
have simp : k = (l.length - n % l.length + k + n) % l.length
Tactic: simp only [mod_add_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n k : ℕ
hk rw : k < l.length
⊢ k = (l.length - n % l.length + k + n) % l.length
have rw₁ : n % l.length ≤ l.length
Tactic: rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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₂
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n h₁ = a
Tactic: rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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₂
have rw₁ : some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n h₁) = some a
Tactic: rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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₂
have rw₂ : getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n = some a
Tactic: rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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₂
have rw₃ : ((a :: l).rotate n).head? = some a
Tactic: rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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₂
have rw₄ : (a :: l).head? = some a
Tactic: rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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₂
have rw₅ : some a = some a
Tactic: rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ (a :: l).rotate n = a :: l
have rw : (replicate (a :: l).length b).rotate n = replicate (a :: l).length b
Tactic: rw [hb, rotate_replicate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ (a :: l).rotate n = a :: l
have rw₁ : replicate (a :: l).length b = replicate (a :: l).length b
Tactic: rw [hb, rotate_replicate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ l.rotate n.succ = l
have rwa₁ : (l.rotate n).rotate 1 = l
Tactic: rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
⊢ l = l'
have hle : l.length = l'.length
Tactic: have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
n : ℕ
l l' : List α
h : l.rotate n = l'.rotate n
hle : l.length = l'.length
⊢ l = l'
have h₁ : 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
Cleared hypotheses: h, hle
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
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
⊢ l = l'
have hd : drop (n % l.length) l = drop (n % l'.length) l'
Tactic: obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
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
hd : drop (n % l.length) l = drop (n % l'.length) l'
⊢ l = l'
have ht : take (n % l.length) l = take (n % l'.length) l'
Tactic: obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l = l'
have rw : take (n % l.length) l ++ drop (n % l.length) l = l'
Tactic: rw [← take_append_drop _ l, ht, hd, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
rw : take (n % l.length) l ++ drop (n % l.length) l = l'
rw₁ : ℕ
⊢ l = l'
have rw₂ : take (n % l'.length) l' ++ drop (n % l.length) l = l'
Tactic: rw [← take_append_drop _ l, ht, hd, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
rw : take (n % l.length) l ++ drop (n % l.length) l = l'
rw₁ : ℕ
rw₂ : take (n % l'.length) l' ++ drop (n % l.length) l = l'
⊢ l = l'
have rw₃ : take (n % l'.length) l' ++ drop (n % l'.length) l' = l'
Tactic: rw [← take_append_drop _ l, ht, hd, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
rw : take (n % l.length) l ++ drop (n % l.length) l = l'
rw₁ : ℕ
rw₂ : take (n % l'.length) l' ++ drop (n % l.length) l = l'
rw₃ : take (n % l'.length) l' ++ drop (n % l'.length) l' = l'
⊢ l = l'
have rw₄ : l' = l'
Tactic: rw [← take_append_drop _ l, ht, hd, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)
have rw : l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Tactic: rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inl : ∀ (hl : 0 = l'.length),
  l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Tactic: rcases l'.length.zero_le.eq_or_lt with hl | hl
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
inl :
  ∀ (hl : 0 = l'.length),
    l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inr : ∀ (hl : 0 < l'.length),
  l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Tactic: rcases l'.length.zero_le.eq_or_lt with hl | hl
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inl : l.rotate n = [] ↔
  l.rotate n =
    rotate []
      (((length.{u} (α := α) [] - n % length.{u} (α := α) []) % length.{u} (α := α) [] + n % length.{u} (α := α) []) %
        length.{u} (α := α) [])
Tactic: rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
inl :
  l.rotate n = [] ↔
    l.rotate n =
      rotate []
        (((length.{u} (α := α) [] - n % length.{u} (α := α) []) % length.{u} (α := α) [] + n % length.{u} (α := α) []) %
          length.{u} (α := α) [])
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inl₁ : l.rotate n = [] ↔ l.rotate n = []
Tactic: rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inr : ∀ (hn : 0 = n % l'.length),
  l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Tactic: rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
inr :
  ∀ (hn : 0 = n % l'.length),
    l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inr₁ : ∀ (hn : 0 < n % l'.length),
  l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Tactic: rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
have inr : n % l'.length ≤ l'.length
Tactic: rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ l = [x]
have rw : l = [x].rotate ([x].length - n % [x].length) ↔ l = [x]
Tactic: rw [rotate_eq_iff, rotate_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
x : α
rw : l = [x].rotate ([x].length - n % [x].length) ↔ l = [x]
⊢ l.rotate n = [x] ↔ l = [x]
have rw₁ : l = [x] ↔ l = [x]
Tactic: rw [rotate_eq_iff, rotate_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = l.rotate n ↔ [x] = l
have rw : l.rotate n = [x] ↔ [x] = l
Tactic: rw [eq_comm, rotate_eq_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
x : α
rw : l.rotate n = [x] ↔ [x] = l
⊢ [x] = l.rotate n ↔ [x] = l
have rw₁ : l = [x] ↔ [x] = l
Tactic: rw [eq_comm, rotate_eq_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
x : α
rw : l.rotate n = [x] ↔ [x] = l
rw₁ : l = [x] ↔ [x] = l
⊢ [x] = l.rotate n ↔ [x] = l
have rw₂ : [x] = l ↔ [x] = l
Tactic: rw [eq_comm, rotate_eq_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)
have rw : (l.rotate n).reverse.rotate n = l.reverse
Tactic: rw [← length_reverse, ← rotate_eq_iff]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse
have succ : Eq.{u + 1} (α := List α) (rotate (reverse (rotate [] (n + 1))) (n + 1)) (reverse [])
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
succ : Eq.{u + 1} (α := List α) (rotate (reverse (rotate [] (n + 1))) (n + 1)) (reverse [])
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse
have succ₁ : ∀ (hd : α) (tl : List α), ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse
have succ : (tl ++ [hd]).reverse.rotate 1 = (hd :: tl).reverse
Tactic: rw [rotate_cons_succ, ← rotate_rotate, hn]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse.rotate n = l.reverse
have zero : ∀ (l : List α), (l.rotate 0).reverse.rotate 0 = l.reverse
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ (l : List α), (l.rotate 0).reverse.rotate 0 = l.reverse
⊢ (l.rotate n).reverse.rotate n = l.reverse
have succ : ∀ (n : ℕ) (hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse) (l : List α),
  (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse
have rw : l.reverse.reverse.reverse.rotate n =
  (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse
Tactic: rw [← reverse_reverse l]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse
have simp_rw : l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))
Tactic: simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
    length_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))
have rw : l.reverse =
  l.reverse.rotate
    (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
      (l.reverse.length - n % l.reverse.length))
Tactic: rw [← length_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
have zero : ∀ (hk' : k = 0),
  l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
Tactic: rcases hk' : k with - | k'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
zero :
  ∀ (hk' : k = 0),
    l.reverse =
      l.reverse.rotate
        (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
          (l.reverse.length - n % l.reverse.length))
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
have succ : ∀ (k' : ℕ) (hk' : k = k' + 1),
  l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
Tactic: rcases hk' : k with - | k'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
have succ : let k := n % length.{u} (α := α) (reverse []);
∀ (hk' : k = k' + 1),
  Eq.{u + 1} (α := List α) (reverse [])
    (rotate (reverse [])
      (length.{u} (α := α) (reverse []) -
          (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse [])) % length.{u} (α := α) (reverse []) +
        (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse []))))
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, k, hk'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
succ :
  let k := n % length.{u} (α := α) (reverse []);
  ∀ (hk' : k = k' + 1),
    Eq.{u + 1} (α := List α) (reverse [])
      (rotate (reverse [])
        (length.{u} (α := α) (reverse []) -
            (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse [])) %
              length.{u} (α := α) (reverse []) +
          (length.{u} (α := α) (reverse []) - n % length.{u} (α := α) (reverse []))))
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))
have succ₁ : ∀ (x : α) (l : List α),
  let k := n % (x :: l).reverse.length;
  ∀ (hk' : k = k' + 1),
    (x :: l).reverse =
      (x :: l).reverse.rotate
        ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
          ((x :: l).reverse.length - n % (x :: l).reverse.length))
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, k, hk'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))
have succ : (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length
Tactic: rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
succ : (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))
have succ₁ : (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
Tactic: rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)
have succ : map f (rotate [] (n + 1)) = (map f []).rotate (n + 1)
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
succ : map f (rotate [] (n + 1)) = (map f []).rotate (n + 1)
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)
have succ₁ : ∀ (hd : α) (tl : List α), map f ((hd :: tl).rotate (n + 1)) = (map f (hd :: tl)).rotate (n + 1)
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
⊢ map f (l.rotate n) = (map f l).rotate n
have zero : ∀ (l : List α), map f (l.rotate 0) = (map f l).rotate 0
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [hn]
Cleared hypotheses: l, n