case intro
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~r l
α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l
obtain ⟨n, rfl⟩ := h
case intro.nil
α : Type u
n : ℕ
⊢ rotate [] n ~r []

case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (hd :: tl) n ~r (hd :: tl)
case intro
α : Type u
l : List α
n : ℕ
⊢ rotate l n ~r l
cases' l with hd tl
no goals
case intro.nil
α : Type u
n : ℕ
⊢ rotate [] n ~r []
exists 0
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (rotate (hd :: tl) n) (length (hd :: tl) * n - n) = hd :: tl
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (hd :: tl) n ~r (hd :: tl)
use (hd :: tl).length * n - n
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ length (hd :: tl) * n
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ rotate (rotate (hd :: tl) n) (length (hd :: tl) * n - n) = hd :: tl
rw [rotate_rotate, add_tsub_cancel_of_le, rotate_length_mul]
no goals
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ length (hd :: tl) * n
exact Nat.le_mul_of_pos_left (by simp)
no goals
α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < length (hd :: tl)
simp