awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
zero : ∀ (l : List α), map f (l.rotate 0) = (map f l).rotate 0
⊢ map f (l.rotate n) = (map f l).rotate n
have succ : ∀ (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)
Tactic: induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [hn]
Cleared hypotheses: l, n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate i = l.rotate j
⊢ i % l.length = j % l.length
have h₁ : l.rotate (i % l.length) = l.rotate (j % l.length)
Tactic: rw [← rotate_mod l i, ← rotate_mod l j] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
have inl : ∀ (hl : Nodup.{u} (α := α) []),
  Eq.{u + 1} (α := List α) (rotate [] i) (rotate [] j) ↔
    i % length.{u} (α := α) [] = j % length.{u} (α := α) [] ∨ Eq.{u + 1} (α := List α) [] []
Tactic: rcases eq_or_ne l [] with rfl | hn
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
inl :
  ∀ (hl : Nodup.{u} (α := α) []),
    Eq.{u + 1} (α := List α) (rotate [] i) (rotate [] j) ↔
      i % length.{u} (α := α) [] = j % length.{u} (α := α) [] ∨ Eq.{u + 1} (α := List α) [] []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
have inr : ∀ (hn : l ≠ []), l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
Tactic: rcases eq_or_ne l [] with rfl | hn
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
have inr : l.rotate i = l.rotate j ↔ i % l.length = j % l.length
Tactic: simp only [hn, or_false]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length
have inr : ∀ (h : i % l.length = j % l.length), l.rotate i = l.rotate j
Tactic: refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate i = l.rotate j
have inr : l.rotate (i % l.length) = l.rotate j
Tactic: rw [← rotate_mod, h, rotate_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
inr : l.rotate (i % l.length) = l.rotate j
⊢ l.rotate i = l.rotate j
have inr₁ : l.rotate (j % l.length) = l.rotate j
Tactic: rw [← rotate_mod, h, rotate_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
inr : l.rotate (i % l.length) = l.rotate j
inr₁ : l.rotate (j % l.length) = l.rotate j
⊢ l.rotate i = l.rotate j
have inr₂ : l.rotate j = l.rotate j
Tactic: rw [← rotate_mod, h, rotate_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []
have rw : l.rotate n = l ↔ n % l.length = 0 % l.length ∨ l = []
Tactic: rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
rw : l.rotate n = l ↔ n % l.length = 0 % l.length ∨ l = []
rw₁ : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []
have rw₂ : l.rotate n = l ↔ l.rotate n = l.rotate 0
Tactic: rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
rw : l.rotate n = l ↔ n % l.length = 0 % l.length ∨ l = []
rw₁ : ℕ
rw₂ : l.rotate n = l ↔ l.rotate n = l.rotate 0
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []
have rw₃ : l.rotate n = l ↔ l.rotate n = l
Tactic: rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l
have obtain : ∀ (n : ℕ), l.rotate n ~r l
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~r l
have nil : IsRotated.{u} (α := α) (rotate [] n) []
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
nil : IsRotated.{u} (α := α) (rotate [] n) []
⊢ l.rotate n ~r l
have cons : ∀ (hd : α) (tl : List α), (hd :: tl).rotate n ~r hd :: tl
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
⊢ IsRotated.{u} (α := α) (rotate [] n) []
have nil : Eq.{u + 1} (α := List α) (rotate (rotate [] n) 0) []
Tactic: exists 0
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl
have h : ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl
Tactic: use (hd :: tl).length * n - n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl
have h : n ≤ (hd :: tl).length * n
Tactic: rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n m : ℕ
⊢ l.rotate (n + m) = (l.rotate n).rotate m
have rw : l.rotate (n + m) = l.rotate (n + m)
Tactic: rw [rotate_rotate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
⊢ [] ~r l ↔ [] = l
have rw : l ~r [] ↔ [] = l
Tactic: rw [isRotated_comm, isRotated_nil_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
rw : l ~r [] ↔ [] = l
⊢ [] ~r l ↔ [] = l
have rw₁ : l = [] ↔ [] = l
Tactic: rw [isRotated_comm, isRotated_nil_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
rw : l ~r [] ↔ [] = l
rw₁ : l = [] ↔ [] = l
⊢ [] ~r l ↔ [] = l
have rw₂ : [] = l ↔ [] = l
Tactic: rw [isRotated_comm, isRotated_nil_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
x : α
⊢ [x] ~r l ↔ [x] = l
have rw : l ~r [x] ↔ [x] = l
Tactic: rw [isRotated_comm, isRotated_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
x : α
rw : l ~r [x] ↔ [x] = l
⊢ [x] ~r l ↔ [x] = l
have rw₁ : l = [x] ↔ [x] = l
Tactic: rw [isRotated_comm, isRotated_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
x : α
rw : l ~r [x] ↔ [x] = l
rw₁ : l = [x] ↔ [x] = l
⊢ [x] ~r l ↔ [x] = l
have rw₂ : [x] = l ↔ [x] = l
Tactic: rw [isRotated_comm, isRotated_singleton_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
h : l ~r l'
⊢ l.reverse ~r l'.reverse
have obtain : ∀ (n : ℕ), l.reverse ~r (l.rotate n).reverse
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ l.reverse ~r l' ↔ l ~r l'.reverse
have mp : l.reverse ~r l' → l ~r l'.reverse
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
mp : l.reverse ~r l' → l ~r l'.reverse
⊢ l.reverse ~r l' ↔ l ~r l'.reverse
have mpr : l ~r l'.reverse → l.reverse ~r l'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'
have refine : ∀ (h : l ~r l'), ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'
Tactic: refine ⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l'
have obtain : ∀ (n : ℕ), ∃ (n_1 : ℕ), n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
⊢ ∃ (n_1 : ℕ), n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n
have nil : ∃ (n_1 : ℕ), n_1 ≤ length.{u} (α := α) [] ∧ Eq.{u + 1} (α := List α) (rotate [] n_1) (rotate [] n)
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
nil : ∃ (n_1 : ℕ), n_1 ≤ length.{u} (α := α) [] ∧ Eq.{u + 1} (α := List α) (rotate [] n_1) (rotate [] n)
⊢ ∃ (n_1 : ℕ), n_1 ≤ l.length ∧ l.rotate n_1 = l.rotate n
have cons : ∀ (hd : α) (tl : List α), ∃ (n_1 : ℕ), n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ (n_1 : ℕ), n_1 ≤ (hd :: tl).length ∧ (hd :: tl).rotate n_1 = (hd :: tl).rotate n
have cons : n % (hd :: tl).length ≤ (hd :: tl).length
Tactic: refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % (hd :: tl).length ≤ (hd :: tl).length
have cons : 0 < (hd :: tl).length
Tactic: refine (Nat.mod_lt _ ?_).le
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))
have simp_rw : (∃ (n : ℕ), n ≤ l.length ∧ l.rotate n = l') ↔ ∃ (a : ℕ), a < l.length + 1 ∧ l.rotate a = l'
Tactic: simp_rw [mem_map, mem_range, isRotated_iff_mod]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂
have obtain : ∀ (n : ℕ), List.map f l₁ ~r List.map f (l₁.rotate n)
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (l₁.rotate n)
have rw : List.map f l₁ ~r (List.map f l₁).rotate n
Tactic: rw [map_rotate]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
β : Type u_1
l₁ : List α
f : α → β
n w : ℕ
⊢ List.map f l₁ ~r (List.map f l₁).rotate n
have h : (List.map f l₁).rotate n = (List.map f l₁).rotate n
Tactic: use n
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : List α
L : α
h : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]
have append_singleton : (if h' : [L].isEmpty = true then a.getLast sorry else [L].getLast sorry) :: a ~r a ++ [L]
Tactic: simp only [getLast_append, dropLast_concat]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
a : List α
L : α
h : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (if h' : [L].isEmpty = true then a.getLast ⋯ else [L].getLast ⋯) :: a ~r a ++ [L]
have append_singleton : a ++ [L] ~r (if h' : [L].isEmpty = true then a.getLast sorry else [L].getLast sorry) :: a
Tactic: apply IsRotated.symm
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
L : List α
hL : L ≠ []
⊢ L.getLast hL :: L.dropLast ~r L
have nil : ∀ (hL : Ne.{u + 1} (α := List α) [] []), getLast [] hL :: dropLast [] ~r []
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
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
L : List α
hL : L ≠ []
nil : ∀ (hL : Ne.{u + 1} (α := List α) [] []), getLast [] hL :: dropLast [] ~r []
⊢ L.getLast hL :: L.dropLast ~r L
have 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]
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
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
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).dropLast ~r (a :: b :: L).tail
have hL'₁ : a = (b :: L).getLast sorry
Tactic: simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'
Cleared hypotheses: hL'
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations = dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) l.tails l.inits)
have obtain : ∀ (hd : α) (tl : List α) (h : hd :: tl ≠ []),
  (hd :: tl).cyclicPermutations = dropLast (zipWith (fun (x1 x2 : List α) ↦ x1 ++ x2) (hd :: tl).tails (hd :: tl).inits)
Tactic: obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
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
have cons : drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n
Tactic: simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n
have cons : drop n (a :: l) ++ take n (a :: l) = drop n (a :: l) ++ take n (a :: l)
Tactic: rw [rotate_eq_drop_append_take (by simpa using h.le)]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.cyclicPermutations.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.cyclicPermutations n h = l.rotate n
have nil : ∀ (h : n < length.{u} (α := List α) (cyclicPermutations [])),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (cyclicPermutations []) n h = 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)]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.cyclicPermutations n h = l.rotate n
have 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
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)]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
⊢ l.cyclicPermutations.head ⋯ = l
have h : 0 < l.cyclicPermutations.length
Tactic: have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.cyclicPermutations.head ⋯ = l
have rw : l.cyclicPermutations.get (⟨0, h⟩ : Fin l.cyclicPermutations.length) = l
Tactic: rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
rw : l.cyclicPermutations.get (⟨0, h⟩ : Fin l.cyclicPermutations.length) = l
⊢ l.cyclicPermutations.head ⋯ = l
have rw₁ : l.rotate (↑(⟨0, h⟩ : Fin l.cyclicPermutations.length) : ℕ) = l
Tactic: rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ l.cyclicPermutations.head ⋯ = l
have rw₂ : l.rotate 0 = l
Tactic: rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ l.cyclicPermutations.head ⋯ = l
have rw₃ : l = l
Tactic: rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
⊢ l.cyclicPermutations.head? = some l
have rw : some (l.cyclicPermutations.head sorry) = some l
Tactic: rw [head?_eq_some_head (cyclicPermutations_ne_nil l), head_cyclicPermutations]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
rw : some (l.cyclicPermutations.head ⋯) = some l
⊢ l.cyclicPermutations.head? = some l
have rw₁ : some l = some l
Tactic: rw [head?_eq_some_head (cyclicPermutations_ne_nil l), head_cyclicPermutations]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l' l : List α
h : l' ∈ l.cyclicPermutations
⊢ l'.length = l.length
have obtain : ∀ (k : Fin l.cyclicPermutations.length) (h : l.cyclicPermutations.get k ∈ l.cyclicPermutations),
  (l.cyclicPermutations.get k).length = l.length
Tactic: obtain ⟨k, hk, rfl⟩ := get_of_mem h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
have nil : length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
  length.{u} (α := List α) (rotate (cyclicPermutations []) k)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
l : List α
k : ℕ
nil :
  length.{u} (α := List α) (cyclicPermutations (rotate [] k)) =
    length.{u} (α := List α) (rotate (cyclicPermutations []) k)
⊢ (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
have cons : ∀ (head : α) (tail : List α),
  ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
k : ℕ
head : α
tail : List α
⊢ ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length
have cons : ((head :: tail).rotate k).length = ((head :: tail).cyclicPermutations.rotate k).length
Tactic: rw [length_cyclicPermutations_of_ne_nil]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
Goal:
α : Type u
k : ℕ
head : α
tail : List α
cons : ((head :: tail).rotate k).length = ((head :: tail).cyclicPermutations.rotate k).length
⊢ ((head :: tail).rotate k).cyclicPermutations.length = ((head :: tail).cyclicPermutations.rotate k).length
have cons₁ : (head :: tail).rotate k ≠ []
Tactic: rw [length_cyclicPermutations_of_ne_nil]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (hypothesis)
Goal:
α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k
have this : (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
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
have 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)
Tactic: refine ext_get this fun n hn hn' => ?_
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ (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)
have 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, sorry⟩
Tactic: rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Rotate (goal)
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
⊢ 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, ⋯⟩
have 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 []),
        sorry⟩)
Tactic: cases l
Cleared hypotheses: l, this, hn, hn'