α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get l
      {
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get (rotate l n)
      { val := (length l - n % length l + ↑k) % length l,
        isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) }
rw [get_rotate]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k =
    ↑{
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ get l k =
    get l
      {
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
refine congr_arg l.get (Fin.eq_of_val_eq ?_)
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k = (length l - n % length l + ↑k + n) % length l
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k =
    ↑{
        val :=
          (↑{ val := (length l - n % length l + ↑k) % length l,
                  isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
              n) %
            length l,
        isLt :=
          (_ :
            (↑{ val := (length l - n % length l + ↑k) % length l,
                      isLt := (_ : (length l - n % length l + ↑k) % length l < length (rotate l n)) } +
                  n) %
                length l <
              length l) }
simp only [mod_add_mod]
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k < length l

α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ n % length l ≤ length l
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k = (length l - n % length l + ↑k + n) % length l
rw [← add_mod_mod, add_right_comm, tsub_add_cancel_of_le, add_mod_left, mod_eq_of_lt]
no goals
α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ ↑k < length l

α : Type u
l : List α
n : ℕ
k : Fin (length l)
⊢ n % length l ≤ length l
exacts [k.2, (mod_lt _ (k.1.zero_le.trans_lt k.2)).le]