-- Mathlib/Data/List/Rotate.lean
theorem getElem?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) :
    (l.rotate n)[m]? = l[(m + n) % l.length]?

Proof state:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m - l.length < l.length

Tactic:
rw [Nat.sub_lt_iff_lt_add' hm']

Result:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m < l.length + l.length

Proof state:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)

Result:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Proof state:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Tactic:
rw [mod_eq_of_lt hm, Nat.add_comm]

Result:
no goals

Proof state:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
have hm' := Nat.sub_le_iff_le_add'.1 hm

Result:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Proof state:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = n % l.length + m - l.length

Tactic:
omega

Result:
no goals

Proof state:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
rw [getElem?_append_left hm, getElem?_drop, ← add_mod_mod]

Result:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Proof state:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?

Tactic:
congr 1

Result:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Proof state:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
rcases lt_or_le m (l.drop (n % l.length)).length with hm | hm

Result:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Proof state:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
rwa [Nat.sub_lt_iff_lt_add hm, length_drop, Nat.sub_add_cancel hlt.le]

Result:
no goals

Proof state:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (l.rotate n)[m]? = l[(m + n) % l.length]?

Tactic:
rw [rotate_eq_drop_append_take_mod]

Result:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Proof state:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ n % l.length + m < l.length + l.length

Tactic:
exact Nat.add_lt_add hlt hml

Result:
no goals

Proof state:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Tactic:
rw [length_drop, Nat.lt_sub_iff_add_lt] at hm

Result:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Proof state:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]

Result:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = n % l.length + m - l.length

Proof state:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
rw [length_drop] at hm

Result:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Proof state:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]

Result:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?

case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Proof state:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
⊢ m - (l.length - n % l.length) = (m + n) % l.length

Tactic:
have : n % length l + m - length l < length l := by
  rw [Nat.sub_lt_iff_lt_add' hm']
  exact Nat.add_lt_add hlt hml

Result:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length