α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (rotate l n)) n = reverse l
α : Type u
l : List α
n : ℕ
⊢ reverse (rotate l n) = rotate (reverse l) (length l - n % length l)
rw [← length_reverse l, ← rotate_eq_iff]
case zero
α : Type u
l✝ l : List α
⊢ rotate (reverse (rotate l zero)) zero = reverse l

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
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (rotate l n)) n = reverse l
induction' n with n hn generalizing l
no goals
case zero
α : Type u
l✝ l : List α
⊢ rotate (reverse (rotate l zero)) zero = reverse l
simp
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 []

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)
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
cases' l with hd tl
no goals
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 []
simp
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)
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)
rw [rotate_cons_succ, Nat.succ_eq_add_one, ← rotate_rotate, hn]
no goals
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)
simp