simp[fintypeArrowEquivVector, Equiv.vectorEquivFin]
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
i : Fin (Fintype.card ι)
f : ι → α
⊢ (fintypeArrowEquivVector f).get i = f (fintypeEquivFin.symm i)
no goals