n : ℕ
α : Type ?u.12116
v : Vector α n
i : Fin n
⊢ ↑i < n
n : ℕ
α : Type ?u.12116
v : Vector α n
i : Fin n
⊢ ↑i < List.length (toList v)
rw [toList_length]
no goals
n : ℕ
α : Type ?u.12116
v : Vector α n
i : Fin n
⊢ ↑i < n
exact i.2