α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (reverse (reverse l))) n =
    reverse (rotate (reverse (reverse l)) (length (reverse (reverse l)) - n % length (reverse (reverse l))))
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse l) n = reverse (rotate l (length l - n % length l))
rw [← reverse_reverse l]
α : Type u
l : List α
n : ℕ
⊢ reverse l = rotate (reverse l) (length l - (length l - n % length l) % length l + (length l - n % length l))
α : Type u
l : List α
n : ℕ
⊢ rotate (reverse (reverse (reverse l))) n =
    reverse (rotate (reverse (reverse l)) (length (reverse (reverse l)) - n % length (reverse (reverse l))))
simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
  length_reverse]
α : Type u
l : List α
n : ℕ
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
α : Type u
l : List α
n : ℕ
⊢ reverse l = rotate (reverse l) (length l - (length l - n % length l) % length l + (length l - n % length l))
rw [← length_reverse l]
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
α : Type u
l : List α
n : ℕ
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
let k := n % l.reverse.length
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
hk' : k = zero
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))

case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
k' : ℕ
hk' : k = succ k'
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
cases' hk' : k with k'
no goals
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
hk' : k = zero
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
simp_all! [length_reverse, ← rotate_rotate]
case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % length (reverse [])
hk' : k = succ k'
⊢ reverse [] =
    rotate (reverse [])
      (length (reverse []) - (length (reverse []) - n % length (reverse [])) % length (reverse []) +
        (length (reverse []) - n % length (reverse [])))

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ reverse (x :: l) =
    rotate (reverse (x :: l))
      (length (reverse (x :: l)) -
          (length (reverse (x :: l)) - n % length (reverse (x :: l))) % length (reverse (x :: l)) +
        (length (reverse (x :: l)) - n % length (reverse (x :: l))))
case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % length (reverse l)
k' : ℕ
hk' : k = succ k'
⊢ reverse l =
    rotate (reverse l)
      (length (reverse l) - (length (reverse l) - n % length (reverse l)) % length (reverse l) +
        (length (reverse l) - n % length (reverse l)))
cases' l with x l
no goals
case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % length (reverse [])
hk' : k = succ k'
⊢ reverse [] =
    rotate (reverse [])
      (length (reverse []) - (length (reverse []) - n % length (reverse [])) % length (reverse []) +
        (length (reverse []) - n % length (reverse [])))
simp
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) ≤ length (reverse (x :: l))

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) < length (reverse (x :: l))
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ reverse (x :: l) =
    rotate (reverse (x :: l))
      (length (reverse (x :: l)) -
          (length (reverse (x :: l)) - n % length (reverse (x :: l))) % length (reverse (x :: l)) +
        (length (reverse (x :: l)) - n % length (reverse (x :: l))))
rw [Nat.mod_eq_of_lt, tsub_add_cancel_of_le, rotate_length]
no goals
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) ≤ length (reverse (x :: l))
exact tsub_le_self
no goals
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ length (reverse (x :: l)) - n % length (reverse (x :: l)) < length (reverse (x :: l))
exact tsub_lt_self (by simp) (by simp_all!)
no goals
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ 0 < length (reverse (x :: l))
simp
no goals
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % length (reverse (x :: l))
hk' : k = succ k'
⊢ 0 < n % length (reverse (x :: l))
simp_all!