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
no goals
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 = []
simp [rotate_cons_succ, hn]