-- Mathlib/Data/List/Rotate.lean
theorem rotate_reverse (l : List α) (n : ℕ) :
    l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Proof state:
case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % [].reverse.length
hk' : k = k' + 1
⊢ [].reverse =
    [].reverse.rotate
      ([].reverse.length - ([].reverse.length - n % [].reverse.length) % [].reverse.length +
        ([].reverse.length - n % [].reverse.length))

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

Tactic:
exact Nat.sub_le _ _

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
rcases hk' : k with - | k'

Result:
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
hk' : k = 0
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Proof state:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Tactic:
exact Nat.sub_lt (by simp) (by simp_all! [k])

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))

Tactic:
rw [← length_reverse l]

Result:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
let k := n % l.reverse.length

Result:
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Proof state:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < n % (x :: l).reverse.length

Tactic:
simp_all! [k]

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Tactic:
rw [← reverse_reverse l]

Result:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.reverse.reverse.reverse.rotate n =
    (l.reverse.reverse.rotate (l.reverse.reverse.length - n % l.reverse.reverse.length)).reverse

Tactic:
simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
  length_reverse]

Result:
α : Type u
l : List α
n : ℕ
⊢ l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))

Proof state:
case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
rcases l with - | ⟨x, l⟩

Result:
case succ.nil
α : Type u
n k' : ℕ
k : ℕ := n % [].reverse.length
hk' : k = k' + 1
⊢ [].reverse =
    [].reverse.rotate
      ([].reverse.length - ([].reverse.length - n % [].reverse.length) % [].reverse.length +
        ([].reverse.length - n % [].reverse.length))

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Proof state:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse =
    (x :: l).reverse.rotate
      ((x :: l).reverse.length - ((x :: l).reverse.length - n % (x :: l).reverse.length) % (x :: l).reverse.length +
        ((x :: l).reverse.length - n % (x :: l).reverse.length))

Tactic:
rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]

Result:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Proof state:
case zero
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
hk' : k = 0
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
simp_all! [k, length_reverse, ← rotate_rotate]

Result:
no goals

Proof state:
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < (x :: l).reverse.length

Tactic:
simp

Result:
no goals