α : Type u_1
β : Type ?u.17
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) i) ∈ toList v
α : Type u_1
β : Type ?u.17
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ get v i ∈ toList v
rw [get_eq_get]
no goals
α : Type u_1
β : Type ?u.17
n : ℕ
a a' : α
i : Fin n
v : Vector α n
⊢ List.get (toList v) (↑(Fin.cast (_ : n = List.length (toList v))) i) ∈ toList v
exact List.get_mem _ _ _