α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ ↑k < length l
α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ get (rotate l n) k = get l { val := (↑k + n) % length l, isLt := (_ : (↑k + n) % length l < length l) }
rw [← Option.some_inj, ← get?_eq_get, ← get?_eq_get, get?_rotate]
no goals
α : Type u
l : List α
n : ℕ
k : Fin (length (rotate l n))
⊢ ↑k < length l
exact k.2.trans_eq (length_rotate _ _)