α : Type u
l : List α
n : ℕ
⊢ rotate' l n ~ l
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~ l
rw [rotate_eq_rotate']
case zero
α : Type u
l✝ l : List α
⊢ rotate' l zero ~ l

case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
l : List α
⊢ rotate' l (succ n) ~ l
α : Type u
l : List α
n : ℕ
⊢ rotate' l n ~ l
induction' n with n hn generalizing l
no goals
case zero
α : Type u
l✝ l : List α
⊢ rotate' l zero ~ l
simp
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
⊢ rotate' [] (succ n) ~ []

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
case succ
α : Type u
l✝ : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
l : List α
⊢ rotate' l (succ n) ~ l
cases' l with hd tl
no goals
case succ.nil
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
⊢ rotate' [] (succ n) ~ []
simp
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
hd : α
tl : List α
⊢ rotate' (tl ++ [hd]) n ~ hd :: tl
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
rw [rotate'_cons_succ]
no goals
case succ.cons
α : Type u
l : List α
n : ℕ
hn : ∀ (l : List α), rotate' l n ~ l
hd : α
tl : List α
⊢ rotate' (tl ++ [hd]) n ~ hd :: tl
exact (hn _).trans (perm_append_singleton _ _)