[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l (n % length l) = rotate l n
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
n : ℕ
⊢ rotate [] n = []
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
l : List α
⊢ rotate l 0 = l
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
n : ℕ
⊢ rotate' [] n = []
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u
⊢ rotate' [] zero = []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
n✝ : ℕ
⊢ rotate' [] (succ n✝) = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l : List α
⊢ rotate' l 0 = l
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
⊢ rotate' [] 0 = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
head✝ : α
tail✝ : List α
⊢ rotate' (head✝ :: tail✝) 0 = head✝ :: tail✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l : List α
a : α
n : ℕ
⊢ rotate' (a :: l) (succ n) = rotate' (l ++ [a]) n
[PROOFSTEP]
simp [rotate']
[GOAL]
α : Type u
x✝ : ℕ
⊢ length (rotate' [] x✝) = length []
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
⊢ length (rotate' (a :: l) (n + 1)) = length (a :: l)
[PROOFSTEP]
rw [List.rotate', length_rotate' (l ++ [a]) n]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
⊢ length (l ++ [a]) = length (a :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
h : n ≤ length []
⊢ rotate' [] n = drop n [] ++ take n []
[PROOFSTEP]
simp [drop_append_of_le_length h]
[GOAL]
α : Type u
l : List α
h : 0 ≤ length l
⊢ rotate' l 0 = drop 0 l ++ take 0 l
[PROOFSTEP]
simp [take_append_of_le_length h]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
[PROOFSTEP]
have hnl : n ≤ l.length := le_of_succ_le_succ h
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
[PROOFSTEP]
have hnl' : n ≤ (l ++ [a]).length := by rw [length_append, length_cons, List.length]; exact le_of_succ_le h
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length (l ++ [a])
[PROOFSTEP]
rw [length_append, length_cons, List.length]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length l + succ 0
[PROOFSTEP]
exact le_of_succ_le h
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
[PROOFSTEP]
rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take, drop_append_of_le_length hnl,
  take_append_of_le_length hnl]
[GOAL]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
m : ℕ
⊢ rotate' (rotate' (a :: l) 0) m = rotate' (a :: l) (0 + m)
[PROOFSTEP]
simp
[GOAL]
α : Type u
n m : ℕ
⊢ rotate' (rotate' [] n) m = rotate' [] (n + m)
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
n m : ℕ
⊢ rotate' (rotate' (a :: l) (n + 1)) m = rotate' (a :: l) (n + 1 + m)
[PROOFSTEP]
rw [rotate'_cons_succ, rotate'_rotate' _ n, add_right_comm, ← rotate'_cons_succ]
[GOAL]
α : Type u
l : List α
⊢ rotate' l (length l) = l
[PROOFSTEP]
rw [rotate'_eq_drop_append_take le_rfl]
[GOAL]
α : Type u
l : List α
⊢ drop (length l) l ++ take (length l) l = l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
⊢ rotate' l (length l * 0) = l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' l (length l * (n + 1)) = rotate' (rotate' l (length l * n)) (length (rotate' l (length l * n)))
[PROOFSTEP]
simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' (rotate' l (length l * n)) (length (rotate' l (length l * n))) = l
[PROOFSTEP]
rw [rotate'_length, rotate'_length_mul l n]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' l (n % length l) = rotate' (rotate' l (n % length l)) (length (rotate' l (n % length l)) * (n / length l))
[PROOFSTEP]
rw [rotate'_length_mul]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' (rotate' l (n % length l)) (length (rotate' l (n % length l)) * (n / length l)) = rotate' l n
[PROOFSTEP]
rw [rotate'_rotate', length_rotate', Nat.mod_add_div]
[GOAL]
α : Type u
l : List α
n : ℕ
h : length l = 0
⊢ rotate l n = rotate' l n
[PROOFSTEP]
simp_all [length_eq_zero]
[GOAL]
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = rotate' l n
[PROOFSTEP]
rw [← rotate'_mod, rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))]
[GOAL]
α : Type u
l : List α
n : ℕ
h : ¬length l = 0
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
simp [rotate]
[GOAL]
α : Type u
l : List α
a : α
n : ℕ
⊢ rotate (a :: l) (succ n) = rotate (l ++ [a]) n
[PROOFSTEP]
rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]
[GOAL]
α : Type u
x✝ : α
n : ℕ
⊢ x✝ ∈ rotate [] n ↔ x✝ ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
x✝ : α
⊢ x✝ ∈ rotate (a :: l) 0 ↔ x✝ ∈ a :: l
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
l : List α
x✝ : α
n : ℕ
⊢ x✝ ∈ rotate (a :: l) (n + 1) ↔ x✝ ∈ a :: l
[PROOFSTEP]
simp [rotate_cons_succ, mem_rotate, or_comm]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ length (rotate l n) = length l
[PROOFSTEP]
rw [rotate_eq_rotate', length_rotate']
[GOAL]
α : Type u
a : α
n k : ℕ
⊢ length (rotate (replicate n a) k) = n
[PROOFSTEP]
rw [length_rotate, length_replicate]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate l n = drop n l ++ take n l
[PROOFSTEP]
rw [rotate_eq_rotate']
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ n ≤ length l → rotate' l n = drop n l ++ take n l
[PROOFSTEP]
exact rotate'_eq_drop_append_take
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
cases' l.length.zero_le.eq_or_lt with hl hl
[GOAL]
case inl
α : Type u
l : List α
n : ℕ
hl : 0 = length l
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
simp [eq_nil_of_length_eq_zero hl.symm]
[GOAL]
case inr
α : Type u
l : List α
n : ℕ
hl : 0 < length l
⊢ rotate l n = drop (n % length l) l ++ take (n % length l) l
[PROOFSTEP]
rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]
[GOAL]
α : Type u
l l' : List α
⊢ rotate (l ++ l') (length l) = l' ++ l
[PROOFSTEP]
rw [rotate_eq_rotate']
[GOAL]
α : Type u
l l' : List α
⊢ rotate' (l ++ l') (length l) = l' ++ l
[PROOFSTEP]
induction l generalizing l'
[GOAL]
case nil
α : Type u
l' : List α
⊢ rotate' ([] ++ l') (length []) = l' ++ []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), rotate' (tail✝ ++ l') (length tail✝) = l' ++ tail✝
l' : List α
⊢ rotate' (head✝ :: tail✝ ++ l') (length (head✝ :: tail✝)) = l' ++ head✝ :: tail✝
[PROOFSTEP]
simp_all [rotate']
[GOAL]
α : Type u
l : List α
n m : ℕ
⊢ rotate (rotate l n) m = rotate l (n + m)
[PROOFSTEP]
rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']
[GOAL]
α : Type u
l : List α
⊢ rotate l (length l) = l
[PROOFSTEP]
rw [rotate_eq_rotate', rotate'_length]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l (length l * n) = l
[PROOFSTEP]
rw [rotate_eq_rotate', rotate'_length_mul]
[GOAL]
α : Type u
inst✝ : Group α
x✝¹ : prod [] = 1
x✝ : ℕ
⊢ prod (rotate [] x✝) = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
⊢ prod (rotate (a :: l) n) = 1
[PROOFSTEP]
have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
⊢ length (a :: l) > 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
hl : prod (a :: l) = 1
n : ℕ
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
[PROOFSTEP]
rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl 
[GOAL]
α : Type u
inst✝ : Group α
a : α
l : List α
n : ℕ
hl : prod (take (n % length (a :: l)) (a :: l) ++ drop (n % length (a :: l)) (a :: l)) = 1
this : n % length (a :: l) ≤ length (a :: l)
⊢ prod (rotate (a :: l) n) = 1
[PROOFSTEP]
rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq, ← one_mul (List.prod _)⁻¹, ←
  hl, List.prod_append, mul_assoc, mul_inv_self, mul_one]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~ l
[PROOFSTEP]
rw [rotate_eq_rotate']
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate' l n ~ l
[PROOFSTEP]
induction' n with n hn generalizing l
[GOAL]
case zero
α : Type u
l✝ l : List α
⊢ rotate' l zero ~ l
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
l : List α
⊢ rotate' l (succ n) ~ l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
⊢ rotate' [] (succ n) ~ []
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
hd : α
tl : List α
⊢ rotate' (hd :: tl) (succ n) ~ hd :: tl
[PROOFSTEP]
rw [rotate'_cons_succ]
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
hd : α
tl : List α
⊢ rotate' (tl ++ [hd]) n ~ hd :: tl
[PROOFSTEP]
exact (hn _).trans (perm_append_singleton _ _)
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate l n = [] ↔ l = []
[PROOFSTEP]
induction' n with n hn generalizing l
[GOAL]
case zero
α : Type u
l✝ l : List α
⊢ rotate l zero = [] ↔ l = []
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ {l : List α}, rotate l n = [] ↔ l = []
l : List α
⊢ rotate l (succ n) = [] ↔ l = []
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ {l : List α}, rotate l n = [] ↔ l = []
⊢ rotate [] (succ n) = [] ↔ [] = []
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ {l : List α}, rotate l n = [] ↔ l = []
hd : α
tl : List α
⊢ rotate (hd :: tl) (succ n) = [] ↔ hd :: tl = []
[PROOFSTEP]
simp [rotate_cons_succ, hn]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ [] = rotate l n ↔ [] = l
[PROOFSTEP]
rw [eq_comm, rotate_eq_nil_iff, eq_comm]
[GOAL]
α✝ : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : length l = length l'
⊢ rotate (zipWith f l l') n = zipWith f (rotate l n) (rotate l' n)
[PROOFSTEP]
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod, h, zipWith_append, ←
  zipWith_distrib_drop, ← zipWith_distrib_take, List.length_zipWith, h, min_self]
[GOAL]
case h
α✝ : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
n : ℕ
h : length l = length l'
⊢ length (drop (n % length l') l) = length (drop (n % length l') l')
[PROOFSTEP]
rw [length_drop, length_drop, h]
[GOAL]
α : Type u
β : Type u_1
f : α → α → β
x y : α
l : List α
⊢ zipWith f (x :: y :: l) (rotate (x :: y :: l) 1) = f x y :: zipWith f (y :: l) (l ++ [x])
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (rotate l n) m = get? l ((m + n) % length l)
[PROOFSTEP]
rw [rotate_eq_drop_append_take_mod]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
rcases lt_or_le m (l.drop (n % l.length)).length with hm | hm
[GOAL]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
rw [get?_append hm, get?_drop, add_comm m, ← mod_add_mod]
[GOAL]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : m < length (drop (n % length l) l)
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
[PROOFSTEP]
rw [length_drop, lt_tsub_iff_left] at hm 
[GOAL]
case inl
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm✝ : m < length l - n % length l
hm : n % length l + m < length l
⊢ get? l (n % length l + m) = get? l ((n % length l + m) % length l)
[PROOFSTEP]
rw [mod_eq_of_lt hm]
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? (drop (n % length l) l ++ take (n % length l) l) m = get? l ((m + n) % length l)
[PROOFSTEP]
rw [get?_append_right hm, get?_take, length_drop]
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ get? l (m - (length l - n % length l)) = get? l ((m + n) % length l)
[PROOFSTEP]
congr 1
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
rw [length_drop] at hm 
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
have hm' := tsub_le_iff_left.1 hm
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
have : n % length l + m - length l < length l
[GOAL]
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m - length l < length l
[PROOFSTEP]
rw [tsub_lt_iff_left hm']
[GOAL]
case this
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
⊢ n % length l + m < length l + length l
[PROOFSTEP]
exact Nat.add_lt_add hlt hml
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = (m + n) % length l
[PROOFSTEP]
conv_rhs => rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
| (m + n) % length l
[PROOFSTEP]
rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
| (m + n) % length l
[PROOFSTEP]
rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
| (m + n) % length l
[PROOFSTEP]
rw [add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ m - (length l - n % length l) = n % length l + m - length l
[PROOFSTEP]
rw [← add_right_inj l.length, ← add_tsub_assoc_of_le, add_tsub_tsub_cancel, add_tsub_cancel_of_le, add_comm]
[GOAL]
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l ≤ n % length l + m
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ n % length l ≤ length l
case inr.e_a.h
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length l - n % length l ≤ m
hlt : n % length l < length l
hm' : length l ≤ n % length l + m
this : n % length l + m - length l < length l
⊢ length l - n % length l ≤ m
[PROOFSTEP]
exacts [hm', hlt.le, hm]
[GOAL]
case inr
α : Type u
l : List α
n m : ℕ
hml : m < length l
hm : length (drop (n % length l) l) ≤ m
hlt : n % length l < length l
⊢ m - length (drop (n % length l) l) < n % length l
[PROOFSTEP]
rwa [tsub_lt_iff_left hm, length_drop, tsub_add_cancel_of_le hlt.le]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ get (rotate l n) k = get l { val := (↑k + n) % length l, isLt := (_ : (↑k + n) % length l < length l) }
[PROOFSTEP]
rw [← Option.some_inj, ← get?_eq_get, ← get?_eq_get, get?_rotate]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ ↑k < length l
[PROOFSTEP]
exact k.2.trans_eq (length_rotate _ _)
[GOAL]
α : Type u
l : List α
n : ℕ
h : n < length l
⊢ head? (rotate l n) = get? l n
[PROOFSTEP]
rw [← get?_zero, get?_rotate (n.zero_le.trans_lt h), zero_add, Nat.mod_eq_of_lt h]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get (rotate l n)
      { val := (length l - n % length l + ↑k) % length l,
        isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) }
[PROOFSTEP]
rw [get_rotate]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get l
      {
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
[PROOFSTEP]
refine congr_arg l.get (Fin.eq_of_val_eq ?_)
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k =
    ↑{
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
[PROOFSTEP]
simp only [mod_add_mod]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k = (length l - n % length l + ↑k + n) % length l
[PROOFSTEP]
rw [← add_mod_mod, add_right_comm, tsub_add_cancel_of_le, add_mod_left, mod_eq_of_lt]
[GOAL]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k < length l
α : Type u l : List α n : ℕ k : Fin (length l) ⊢ n % length l ≤ length l
[PROOFSTEP]
exacts [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]
[GOAL]
α : Type u
hα : Nonempty α
⊢ (∀ (n : ℕ), rotate [] n = []) ↔ ∃ a, [] = replicate (length []) a
[PROOFSTEP]
simp
[GOAL]
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), rotate (a :: l) n = a :: l
n : ℕ
h₁ : n < length (a :: l)
h₂ : n < length (replicate (length (a :: l)) a)
⊢ get (a :: l) { val := n, isLt := h₁ } = get (replicate (length (a :: l)) a) { val := n, isLt := h₂ }
[PROOFSTEP]
rw [get_replicate, ← Option.some_inj, ← get?_eq_get, ← head?_rotate h₁, h, head?_cons]
[GOAL]
α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (length (a :: l)) a_1
n : ℕ
b : α
hb : a :: l = replicate (length (a :: l)) b
⊢ rotate (a :: l) n = a :: l
[PROOFSTEP]
rw [hb, rotate_replicate]
[GOAL]
α : Type u
inst✝ : Nonempty α
l : List α
h : rotate l 1 = l
n✝ n : ℕ
hn : rotate l n = l
⊢ rotate l (succ n) = l
[PROOFSTEP]
rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]
[GOAL]
α : Type u
n : ℕ
⊢ Injective fun l => rotate l n
[PROOFSTEP]
rintro l l' (h : l.rotate n = l'.rotate n)
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
⊢ l = l'
[PROOFSTEP]
have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : rotate l n = rotate l' n
hle : length l = length l'
⊢ l = l'
[PROOFSTEP]
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h 
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ l = l'
[PROOFSTEP]
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
[GOAL]
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
⊢ length (drop (n % length l) l) = length (drop (n % length l') l')
[PROOFSTEP]
simp_all
[GOAL]
case intro
α : Type u
n : ℕ
l l' : List α
h : drop (n % length l) l ++ take (n % length l) l = drop (n % length l') l' ++ take (n % length l') l'
hle : length l = length l'
hd : drop (n % length l) l = drop (n % length l') l'
ht : take (n % length l) l = take (n % length l') l'
⊢ l = l'
[PROOFSTEP]
rw [← take_append_drop _ l, ht, hd, take_append_drop]
[GOAL]
α : Type u
l l' : List α
n : ℕ
⊢ rotate l n = l' ↔ l = rotate l' (length l' - n % length l')
[PROOFSTEP]
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
[GOAL]
α : Type u
l l' : List α
n : ℕ
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
cases' l'.length.zero_le.eq_or_lt with hl hl
[GOAL]
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil, rotate_eq_nil_iff]
[GOAL]
case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
cases' (Nat.zero_le (n % l'.length)).eq_or_lt with hn hn
[GOAL]
case inr.inl
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
hn : 0 = n % length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
simp [← hn]
[GOAL]
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
hn : 0 < n % length l'
⊢ rotate l n = l' ↔ rotate l n = rotate l' (((length l' - n % length l') % length l' + n % length l') % length l')
[PROOFSTEP]
rw [mod_eq_of_lt (tsub_lt_self hl hn), tsub_add_cancel_of_le, mod_self, rotate_zero]
[GOAL]
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < length l'
hn : 0 < n % length l'
⊢ n % length l' ≤ length l'
[PROOFSTEP]
exact (Nat.mod_lt _ hl).le
[GOAL]
α : Type u
l : List α
n : ℕ
x : α
⊢ rotate l n = [x] ↔ l = [x]
[PROOFSTEP]
rw [rotate_eq_iff, rotate_singleton]
[GOAL]
α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = rotate l n ↔ [x] = l
[PROOFSTEP]
rw [eq_comm, rotate_eq_singleton_iff, eq_comm]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ reverse (rotate l n) = rotate (reverse l) (length l - n % length l)
[PROOFSTEP]
rw [← length_reverse l, ← rotate_eq_iff]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (rotate l n)) n = reverse l
[PROOFSTEP]
induction' n with n hn generalizing l
[GOAL]
case zero
α : Type u
l✝ l : List α
⊢ rotate (reverse (rotate l zero)) zero = reverse l
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
l : List α
⊢ rotate (reverse (rotate l (succ n))) (succ n) = reverse l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
⊢ rotate (reverse (rotate [] (succ n))) (succ n) = reverse []
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
hd : α
tl : List α
⊢ rotate (reverse (rotate (hd :: tl) (succ n))) (succ n) = reverse (hd :: tl)
[PROOFSTEP]
rw [rotate_cons_succ, Nat.succ_eq_add_one, ← rotate_rotate, hn]
[GOAL]
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate (reverse (rotate l n)) n = reverse l
hd : α
tl : List α
⊢ rotate (reverse (tl ++ [hd])) 1 = reverse (hd :: tl)
[PROOFSTEP]
simp
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse l) n = reverse (rotate l (length l - n % length l))
[PROOFSTEP]
rw [← reverse_reverse l]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (reverse (reverse l))) n =
    reverse (rotate (reverse (reverse l)) (length (reverse (reverse l)) - n % length (reverse (reverse l))))
[PROOFSTEP]
simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate, length_reverse]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ reverse l = rotate (reverse l) (length l - (length l - n % length l) % length l + (length l - n % length l))
[PROOFSTEP]
rw [← length_reverse l]
[GOAL]
α : Type u
l : List α
n : ℕ
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
let k := n % l.reverse.length
[GOAL]
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
cases' hk' : k with k'
[GOAL]
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
hk' : k = zero
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
simp_all! [length_reverse, ← rotate_rotate]
[GOAL]
case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
k' : ℕ
hk' : k = succ k'
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
[PROOFSTEP]
cases' l with x l
[GOAL]
case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % length (reverse [])
hk' : k = succ k'
⊢ reverse [] =
    rotate (reverse [])
      (length (reverse []) - (length (reverse []) - n % length (reverse [])) % length (reverse []) +
        (length (reverse []) - n % length (reverse [])))
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ reverse (x :: l) =
    rotate (reverse (x :: l))
      (length (reverse (x :: l)) -
          (length (reverse (x :: l)) - n % length (reverse (x :: l))) % length (reverse (x :: l)) +
        (length (reverse (x :: l)) - n % length (reverse (x :: l))))
[PROOFSTEP]
rw [Nat.mod_eq_of_lt, tsub_add_cancel_of_le, rotate_length]
[GOAL]
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) ≤ length (reverse (x :: l))
[PROOFSTEP]
exact tsub_le_self
[GOAL]
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) < length (reverse (x :: l))
[PROOFSTEP]
exact tsub_lt_self (by simp) (by simp_all! )
[GOAL]
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ 0 < length (reverse (x :: l))
[PROOFSTEP]
simp
[GOAL]
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ 0 < n % length (reverse (x :: l))
[PROOFSTEP]
simp_all!
[GOAL]
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
⊢ map f (rotate l n) = rotate (map f l) n
[PROOFSTEP]
induction' n with n hn IH generalizing l
[GOAL]
case zero
α : Type u
β : Type u_1
f : α → β
l✝ l : List α
⊢ map f (rotate l zero) = rotate (map f l) zero
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type u_1
f : α → β
l✝ : List α
n : ℕ
hn : ∀ (l : List α), map f (rotate l n) = rotate (map f l) n
l : List α
⊢ map f (rotate l (succ n)) = rotate (map f l) (succ n)
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case succ.nil
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
hn : ∀ (l : List α), map f (rotate l n) = rotate (map f l) n
⊢ map f (rotate [] (succ n)) = rotate (map f []) (succ n)
[PROOFSTEP]
simp
[GOAL]
case succ.cons
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
hn : ∀ (l : List α), map f (rotate l n) = rotate (map f l) n
hd : α
tl : List α
⊢ map f (rotate (hd :: tl) (succ n)) = rotate (map f (hd :: tl)) (succ n)
[PROOFSTEP]
simp [hn]
[GOAL]
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l ↔ n % length l = 0 ∨ l = []
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ rotate l n = l → n % length l = 0 ∨ l = []
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
⊢ n % length l = 0 ∨ l = []
[PROOFSTEP]
cases' l.length.zero_le.eq_or_lt with hl' hl'
[GOAL]
case mp.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 = length l
⊢ n % length l = 0 ∨ l = []
[PROOFSTEP]
simp [← length_eq_zero, ← hl']
[GOAL]
case mp.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0 ∨ l = []
[PROOFSTEP]
left
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
[PROOFSTEP]
rw [nodup_iff_nthLe_inj] at hl 
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ n % length l = 0
[PROOFSTEP]
refine' hl _ _ (mod_lt _ hl') hl' _
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe l (n % length l) (_ : n % length l < length l) = nthLe l 0 hl'
[PROOFSTEP]
rw [← nthLe_rotate' _ n]
[GOAL]
case mp.inr.h
α : Type u
l : List α
hl : ∀ (i j : ℕ) (h₁ : i < length l) (h₂ : j < length l), nthLe l i h₁ = nthLe l j h₂ → i = j
n : ℕ
h : rotate l n = l
hl' : 0 < length l
⊢ nthLe (rotate l n) ((length l - n % length l + n % length l) % length l)
      (_ : (length l - n % length l + n % length l) % length l < length (rotate l n)) =
    nthLe l 0 hl'
[PROOFSTEP]
simp_rw [h, tsub_add_cancel_of_le (mod_lt _ hl').le, mod_self]
[GOAL]
case mpr
α : Type u
l : List α
hl : Nodup l
n : ℕ
⊢ n % length l = 0 ∨ l = [] → rotate l n = l
[PROOFSTEP]
rintro (h | h)
[GOAL]
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l n = l
[PROOFSTEP]
rw [← rotate_mod, h]
[GOAL]
case mpr.inl
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : n % length l = 0
⊢ rotate l 0 = l
[PROOFSTEP]
exact rotate_zero l
[GOAL]
case mpr.inr
α : Type u
l : List α
hl : Nodup l
n : ℕ
h : l = []
⊢ rotate l n = l
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
⊢ i % length l = j % length l
[PROOFSTEP]
have hi : i % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
⊢ i % length l = j % length l
[PROOFSTEP]
have hj : j % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hn)
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ i % length l = j % length l
[PROOFSTEP]
refine' (nodup_iff_nthLe_inj.mp hl) _ _ hi hj _
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe l (i % length l) hi = nthLe l (j % length l) hj
[PROOFSTEP]
rw [← nthLe_rotate' l i, ← nthLe_rotate' l j]
[GOAL]
α : Type u
l : List α
hl : Nodup l
hn : l ≠ []
i j : ℕ
h : rotate l i = rotate l j
hi : i % length l < length l
hj : j % length l < length l
⊢ nthLe (rotate l i) ((length l - i % length l + i % length l) % length l)
      (_ : (length l - i % length l + i % length l) % length l < length (rotate l i)) =
    nthLe (rotate l j) ((length l - j % length l + j % length l) % length l)
      (_ : (length l - j % length l + j % length l) % length l < length (rotate l j))
[PROOFSTEP]
simp [tsub_add_cancel_of_le, hi.le, hj.le, h]
[GOAL]
α : Type u
l✝ l' l : List α
⊢ rotate l 0 = l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~r l
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case intro.nil
α : Type u
n : ℕ
⊢ rotate [] n ~r []
[PROOFSTEP]
exists 0
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (hd :: tl) n ~r (hd :: tl)
[PROOFSTEP]
use(hd :: tl).length * n - n
[GOAL]
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (rotate (hd :: tl) n) (length (hd :: tl) * n - n) = hd :: tl
[PROOFSTEP]
rw [rotate_rotate, add_tsub_cancel_of_le, rotate_length_mul]
[GOAL]
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ length (hd :: tl) * n
[PROOFSTEP]
exact Nat.le_mul_of_pos_left (by simp)
[GOAL]
α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < length (hd :: tl)
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' l✝ : List α
n m : ℕ
⊢ rotate l✝ (n + m) = rotate (rotate l✝ n) m
[PROOFSTEP]
rw [rotate_rotate]
[GOAL]
α : Type u
l l' : List α
x✝ : l ~r []
n : ℕ
hn : rotate l n = []
⊢ l = []
[PROOFSTEP]
simpa using hn
[GOAL]
α : Type u
l l' : List α
h : l = []
⊢ l ~r l
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l l' : List α
⊢ [] ~r l ↔ [] = l
[PROOFSTEP]
rw [isRotated_comm, isRotated_nil_iff, eq_comm]
[GOAL]
α : Type u
l l' : List α
x : α
x✝ : l ~r [x]
n : ℕ
hn : rotate l n = [x]
⊢ l = [x]
[PROOFSTEP]
simpa using hn
[GOAL]
α : Type u
l l' : List α
x : α
h : l = [x]
⊢ l ~r l
[PROOFSTEP]
rfl
[GOAL]
α : Type u
l l' : List α
x : α
⊢ [x] ~r l ↔ [x] = l
[PROOFSTEP]
rw [isRotated_comm, isRotated_singleton_iff, eq_comm]
[GOAL]
α : Type u
l l' : List α
hd : α
tl : List α
⊢ rotate (hd :: tl) 1 = tl ++ [hd]
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
⊢ rotate (l ++ l') (length l) = l' ++ l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
h : l ~r l'
⊢ List.reverse l ~r List.reverse l'
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l : List α
n : ℕ
⊢ List.reverse l ~r List.reverse (rotate l n)
[PROOFSTEP]
exact ⟨_, (reverse_rotate _ _).symm⟩
[GOAL]
α : Type u
l l' : List α
⊢ reverse l ~r l' ↔ l ~r reverse l'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
l l' : List α
⊢ reverse l ~r l' → l ~r reverse l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
l l' : List α
h : reverse l ~r l'
⊢ l ~r reverse l'
[PROOFSTEP]
simpa using h.reverse
[GOAL]
case mpr
α : Type u
l l' : List α
⊢ l ~r reverse l' → reverse l ~r l'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
l l' : List α
h : l ~r reverse l'
⊢ reverse l ~r l'
[PROOFSTEP]
simpa using h.reverse
[GOAL]
α : Type u
l l' : List α
⊢ reverse l ~r reverse l' ↔ l ~r l'
[PROOFSTEP]
simp [isRotated_reverse_comm_iff]
[GOAL]
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n, n ≤ length l ∧ rotate l n = l'
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
[GOAL]
α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n, n ≤ length l ∧ rotate l n = l'
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1, n_1 ≤ length l ∧ rotate l n_1 = rotate l n
[PROOFSTEP]
cases' l with hd tl
[GOAL]
case intro.nil
α : Type u
n : ℕ
⊢ ∃ n_1, n_1 ≤ length [] ∧ rotate [] n_1 = rotate [] n
[PROOFSTEP]
simp
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1, n_1 ≤ length (hd :: tl) ∧ rotate (hd :: tl) n_1 = rotate (hd :: tl) n
[PROOFSTEP]
refine' ⟨n % (hd :: tl).length, _, rotate_mod _ _⟩
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % length (hd :: tl) ≤ length (hd :: tl)
[PROOFSTEP]
refine' (Nat.mod_lt _ _).le
[GOAL]
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ length (hd :: tl) > 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map (rotate l) (range (length l + 1))
[PROOFSTEP]
simp_rw [mem_map, mem_range, isRotated_iff_mod]
[GOAL]
α : Type u
l l' : List α
⊢ (∃ n, n ≤ length l ∧ rotate l n = l') ↔ ∃ a, a < length l + 1 ∧ rotate l a = l'
[PROOFSTEP]
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⟩⟩
[GOAL]
α : Type u
l l' : List α
β : Type u_1
l₁ l₂ : List α
h : l₁ ~r l₂
f : α → β
⊢ List.map f l₁ ~r List.map f l₂
[PROOFSTEP]
obtain ⟨n, rfl⟩ := h
[GOAL]
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r List.map f (rotate l₁ n)
[PROOFSTEP]
rw [map_rotate]
[GOAL]
case intro
α : Type u
l l' : List α
β : Type u_1
l₁ : List α
f : α → β
n : ℕ
⊢ List.map f l₁ ~r rotate (List.map f l₁) n
[PROOFSTEP]
use n
[GOAL]
α : Type u
l✝ l' l : List α
h : l ≠ []
⊢ cyclicPermutations l = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails l) (inits l))
[PROOFSTEP]
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h
[GOAL]
case intro.intro
α : Type u
l l' : List α
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ cyclicPermutations (hd :: tl) = dropLast (zipWith (fun x x_1 => x ++ x_1) (tails (hd :: tl)) (inits (hd :: tl)))
[PROOFSTEP]
exact cyclicPermutations_cons _ _
[GOAL]
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ length (cyclicPermutations (x :: l)) = length l + 1
[PROOFSTEP]
simp [cyclicPermutations_cons]
[GOAL]
α : Type u
l✝ l' l : List α
h : l ≠ []
⊢ length (cyclicPermutations l) = length l
[PROOFSTEP]
simp [cyclicPermutations_of_ne_nil _ h]
[GOAL]
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
[PROOFSTEP]
obtain rfl | h := eq_or_ne l []
[GOAL]
case inl
α : Type u
l l' : List α
n : ℕ
hn : n < length (cyclicPermutations [])
⊢ nthLe (cyclicPermutations []) n hn = rotate [] n
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn : n < length (cyclicPermutations l)
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn = rotate l n
[PROOFSTEP]
rw [length_cyclicPermutations_of_ne_nil _ h] at hn 
[GOAL]
case inr
α : Type u
l✝ l' l : List α
n : ℕ
hn✝ : n < length (cyclicPermutations l)
hn : n < length l
h : l ≠ []
⊢ nthLe (cyclicPermutations l) n hn✝ = rotate l n
[PROOFSTEP]
simp [dropLast_eq_take, cyclicPermutations_of_ne_nil _ h, nthLe_take', rotate_eq_drop_append_take hn.le]
[GOAL]
α : Type u
l✝ l' l : List α
⊢ l ∈ cyclicPermutations l
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
α : Type u
l l' : List α
⊢ [] ∈ cyclicPermutations []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ x :: l ∈ cyclicPermutations (x :: l)
[PROOFSTEP]
rw [mem_iff_nthLe]
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ ∃ n h, nthLe (cyclicPermutations (x :: l)) n h = x :: l
[PROOFSTEP]
refine' ⟨0, by simp, _⟩
[GOAL]
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ 0 < length (cyclicPermutations (x :: l))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
⊢ nthLe (cyclicPermutations (x :: l)) 0 (_ : 0 < length (cyclicPermutations (x :: l))) = x :: l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l' l : List α
h : l' ∈ cyclicPermutations l
⊢ length l' = length l
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
[GOAL]
case intro.intro
α : Type u
l✝ l : List α
k : ℕ
hk : k < length (cyclicPermutations l)
h : nthLe (cyclicPermutations l) k hk ∈ cyclicPermutations l
⊢ length (nthLe (cyclicPermutations l) k hk) = length l
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
l✝ l'✝ l l' : List α
⊢ l ∈ cyclicPermutations l' → l ~r l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
l✝ l'✝ l l' : List α
h : l ∈ cyclicPermutations l'
⊢ l ~r l'
[PROOFSTEP]
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem h
[GOAL]
case mp.intro.intro
α : Type u
l l'✝ l' : List α
k : ℕ
hk : k < length (cyclicPermutations l')
h : nthLe (cyclicPermutations l') k hk ∈ cyclicPermutations l'
⊢ nthLe (cyclicPermutations l') k hk ~r l'
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u
l✝ l'✝ l l' : List α
⊢ l ~r l' → l ∈ cyclicPermutations l'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
l✝ l'✝ l l' : List α
h : l ~r l'
⊢ l ∈ cyclicPermutations l'
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h.symm
[GOAL]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ rotate l' k ∈ cyclicPermutations l'
[PROOFSTEP]
rw [mem_iff_nthLe]
[GOAL]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n h, nthLe (cyclicPermutations l') n h = rotate l' k
[PROOFSTEP]
simp only [exists_prop, nthLe_cyclicPermutations]
[GOAL]
case mpr.intro
α : Type u
l l'✝ l' : List α
k : ℕ
h : rotate l' k ~r l'
⊢ ∃ n, n < length (cyclicPermutations l') ∧ rotate l' n = rotate l' k
[PROOFSTEP]
cases' l' with x l
[GOAL]
case mpr.intro.nil
α : Type u
l l' : List α
k : ℕ
h : rotate [] k ~r []
⊢ ∃ n, n < length (cyclicPermutations []) ∧ rotate [] n = rotate [] k
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ ∃ n, n < length (cyclicPermutations (x :: l)) ∧ rotate (x :: l) n = rotate (x :: l) k
[PROOFSTEP]
refine' ⟨k % length (x :: l), _, rotate_mod _ _⟩
[GOAL]
case mpr.intro.cons
α : Type u
l✝ l' : List α
k : ℕ
x : α
l : List α
h : rotate (x :: l) k ~r (x :: l)
⊢ k % length (x :: l) < length (cyclicPermutations (x :: l))
[PROOFSTEP]
simpa using Nat.mod_lt _ (zero_lt_succ _)
[GOAL]
α : Type u
l✝ l' l : List α
⊢ cyclicPermutations l = [[]] ↔ l = []
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by simp [h]⟩
[GOAL]
α : Type u
l✝ l' l : List α
h : l = []
⊢ cyclicPermutations l = [[]]
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
l✝ l' l : List α
h : cyclicPermutations l = [[]]
⊢ l = []
[PROOFSTEP]
rw [eq_comm, ← isRotated_nil_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
[GOAL]
α : Type u
l✝ l' l : List α
x : α
⊢ cyclicPermutations l = [[x]] ↔ l = [x]
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by simp [cyclicPermutations, h, dropLast_eq_take]⟩
[GOAL]
α : Type u
l✝ l' l : List α
x : α
h : l = [x]
⊢ cyclicPermutations l = [[x]]
[PROOFSTEP]
simp [cyclicPermutations, h, dropLast_eq_take]
[GOAL]
α : Type u
l✝ l' l : List α
x : α
h : cyclicPermutations l = [[x]]
⊢ l = [x]
[PROOFSTEP]
rw [eq_comm, ← isRotated_singleton_iff', ← mem_cyclicPermutations_iff, h, mem_singleton]
[GOAL]
α : Type u
l✝ l' l : List α
hn : Nodup l
⊢ Nodup (List.cyclicPermutations l)
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
α : Type u
l l' : List α
hn : Nodup []
⊢ Nodup (List.cyclicPermutations [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ Nodup (List.cyclicPermutations (x :: l))
[PROOFSTEP]
rw [nodup_iff_nthLe_inj]
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
⊢ ∀ (i j : ℕ) (h₁ : i < length (List.cyclicPermutations (x :: l))) (h₂ : j < length (List.cyclicPermutations (x :: l))),
    nthLe (List.cyclicPermutations (x :: l)) i h₁ = nthLe (List.cyclicPermutations (x :: l)) j h₂ → i = j
[PROOFSTEP]
intro i j hi hj h
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi : i < length (List.cyclicPermutations (x :: l))
hj : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi = nthLe (List.cyclicPermutations (x :: l)) j hj
⊢ i = j
[PROOFSTEP]
simp only [length_cyclicPermutations_cons] at hi hj 
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i = j
[PROOFSTEP]
rw [← mod_eq_of_lt hi, ← mod_eq_of_lt hj]
[GOAL]
case cons
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ i % (length l + 1) = j % (length l + 1)
[PROOFSTEP]
apply hn.rotate_congr
[GOAL]
case cons.hn
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ x :: l ≠ []
[PROOFSTEP]
simp
[GOAL]
case cons.h
α : Type u
l✝ l' : List α
x : α
l : List α
hn : Nodup (x :: l)
i j : ℕ
hi✝ : i < length (List.cyclicPermutations (x :: l))
hj✝ : j < length (List.cyclicPermutations (x :: l))
h : nthLe (List.cyclicPermutations (x :: l)) i hi✝ = nthLe (List.cyclicPermutations (x :: l)) j hj✝
hi : i < length l + 1
hj : j < length l + 1
⊢ rotate (x :: l) i = rotate (x :: l) j
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
⊢ cyclicPermutations (rotate l k) = rotate (cyclicPermutations l) k
[PROOFSTEP]
have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) :=
  by
  cases l
  · simp
  · rw [length_cyclicPermutations_of_ne_nil] <;> simp
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
⊢ length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
l l' : List α
k : ℕ
⊢ length (cyclicPermutations (rotate [] k)) = length (rotate (cyclicPermutations []) k)
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ length (cyclicPermutations (rotate (head✝ :: tail✝) k)) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
[PROOFSTEP]
rw [length_cyclicPermutations_of_ne_nil]
[GOAL]
case cons
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ length (rotate (head✝ :: tail✝) k) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
[PROOFSTEP]
simp
[GOAL]
case cons.h
α : Type u
l l' : List α
k : ℕ
head✝ : α
tail✝ : List α
⊢ rotate (head✝ :: tail✝) k ≠ []
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
⊢ cyclicPermutations (rotate l k) = rotate (cyclicPermutations l) k
[PROOFSTEP]
refine' ext_nthLe this fun n hn hn' => _
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ nthLe (cyclicPermutations (rotate l k)) n hn = nthLe (rotate (cyclicPermutations l) k) n hn'
[PROOFSTEP]
rw [nthLe_rotate, nthLe_cyclicPermutations, rotate_rotate, ← rotate_mod, add_comm]
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
this : length (cyclicPermutations (rotate l k)) = length (rotate (cyclicPermutations l) k)
n : ℕ
hn : n < length (cyclicPermutations (rotate l k))
hn' : n < length (rotate (cyclicPermutations l) k)
⊢ rotate l ((n + k) % length l) =
    nthLe (cyclicPermutations l) ((n + k) % length (cyclicPermutations l))
      (_ : (n + k) % length (cyclicPermutations l) < length (cyclicPermutations l))
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
l l' : List α
k n : ℕ
this : length (cyclicPermutations (rotate [] k)) = length (rotate (cyclicPermutations []) k)
hn : n < length (cyclicPermutations (rotate [] k))
hn' : n < length (rotate (cyclicPermutations []) k)
⊢ rotate [] ((n + k) % length []) =
    nthLe (cyclicPermutations []) ((n + k) % length (cyclicPermutations []))
      (_ : (n + k) % length (cyclicPermutations []) < length (cyclicPermutations []))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
l l' : List α
k n : ℕ
head✝ : α
tail✝ : List α
this : length (cyclicPermutations (rotate (head✝ :: tail✝) k)) = length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
hn : n < length (cyclicPermutations (rotate (head✝ :: tail✝) k))
hn' : n < length (rotate (cyclicPermutations (head✝ :: tail✝)) k)
⊢ rotate (head✝ :: tail✝) ((n + k) % length (head✝ :: tail✝)) =
    nthLe (cyclicPermutations (head✝ :: tail✝)) ((n + k) % length (cyclicPermutations (head✝ :: tail✝)))
      (_ : (n + k) % length (cyclicPermutations (head✝ :: tail✝)) < length (cyclicPermutations (head✝ :: tail✝)))
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l'✝ l l' : List α
h : l ~r l'
⊢ List.cyclicPermutations l ~r List.cyclicPermutations l'
[PROOFSTEP]
obtain ⟨k, rfl⟩ := h
[GOAL]
case intro
α : Type u
l✝ l' l : List α
k : ℕ
⊢ List.cyclicPermutations l ~r List.cyclicPermutations (rotate l k)
[PROOFSTEP]
exact ⟨k, by simp⟩
[GOAL]
α : Type u
l✝ l' l : List α
k : ℕ
⊢ rotate (List.cyclicPermutations l) k = List.cyclicPermutations (rotate l k)
[PROOFSTEP]
simp
[GOAL]
α : Type u
l✝ l'✝ l l' : List α
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
by_cases hl : l = []
[GOAL]
case pos
α : Type u
l✝ l'✝ l l' : List α
hl : l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
simp [hl, eq_comm]
[GOAL]
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
have hl' : l.cyclicPermutations.length = l.length := length_cyclicPermutations_of_ne_nil _ hl
[GOAL]
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
⊢ cyclicPermutations l ~r cyclicPermutations l' ↔ l ~r l'
[PROOFSTEP]
refine' ⟨fun h => _, IsRotated.cyclicPermutations⟩
[GOAL]
case neg
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
h : cyclicPermutations l ~r cyclicPermutations l'
⊢ l ~r l'
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ l ~r l'
[PROOFSTEP]
refine' ⟨k % l.length, _⟩
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
⊢ rotate l (k % length l) = l'
[PROOFSTEP]
have hk' : k % l.length < l.length := mod_lt _ (length_pos_of_ne_nil hl)
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ rotate l (k % length l) = l'
[PROOFSTEP]
rw [← nthLe_cyclicPermutations _ _ (hk'.trans_le hl'.ge), ← nthLe_rotate' _ k]
[GOAL]
case neg.intro
α : Type u
l✝ l'✝ l l' : List α
hl : ¬l = []
hl' : length (cyclicPermutations l) = length l
k : ℕ
hk : rotate (cyclicPermutations l) k = cyclicPermutations l'
hk' : k % length l < length l
⊢ nthLe (rotate (cyclicPermutations l) k)
      ((length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
        length (cyclicPermutations l))
      (_ :
        (length (cyclicPermutations l) - k % length (cyclicPermutations l) + k % length l) %
            length (cyclicPermutations l) <
          length (rotate (cyclicPermutations l) k)) =
    l'
[PROOFSTEP]
simp [hk, hl', tsub_add_cancel_of_le hk'.le]
