α : Type u
l l' : List α
⊢ rotate' (l ++ l') (length l) = l' ++ l
α : Type u
l l' : List α
⊢ rotate (l ++ l') (length l) = l' ++ l
rw [rotate_eq_rotate']
case nil
α : Type u
l' : List α
⊢ rotate' ([] ++ l') (length []) = l' ++ []

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✝
α : Type u
l l' : List α
⊢ rotate' (l ++ l') (length l) = l' ++ l
induction l generalizing l'
no goals
case nil
α : Type u
l' : List α
⊢ rotate' ([] ++ l') (length []) = l' ++ []
simp
no goals
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✝
simp_all [rotate']