case zero
α : Type u
β : Type u_1
f : α → β
l✝ l : List α
⊢ map f (rotate l zero) = rotate (map f l) zero

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)
α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
⊢ map f (rotate l n) = rotate (map f l) n
induction' n with n hn IH generalizing l
no goals
case zero
α : Type u
β : Type u_1
f : α → β
l✝ l : List α
⊢ map f (rotate l zero) = rotate (map f l) zero
simp
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)

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)
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)
cases' l with hd tl
no goals
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)
simp
no goals
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)
simp [hn]