α : Type u_1
β : Type ?u.364270
γ : Type ?u.364273
σ : Type ?u.364276
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
a : Vector α n × Fin n
⊢ List.get? (Vector.toList a.fst) ↑a.snd =
    List.get? (Vector.toList a.fst) ↑(↑(Fin.cast (_ : n = List.length (Vector.toList a.fst))) a.snd)
α : Type u_1
β : Type ?u.364270
γ : Type ?u.364273
σ : Type ?u.364276
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
a : Vector α n × Fin n
⊢ List.get? (Vector.toList a.fst) ↑a.snd = some (Vector.get a.fst a.snd)
rw [Vector.get_eq_get, ← List.get?_eq_get]
no goals
α : Type u_1
β : Type ?u.364270
γ : Type ?u.364273
σ : Type ?u.364276
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
a : Vector α n × Fin n
⊢ List.get? (Vector.toList a.fst) ↑a.snd =
    List.get? (Vector.toList a.fst) ↑(↑(Fin.cast (_ : n = List.length (Vector.toList a.fst))) a.snd)
rfl