simp[hk]
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
k : ℕ
hk : Fintype.card (Fin k) = k
v : Fin k → α
i : Fin k
⊢ (fintypeArrowEquivFinArrow' hk).symm v i = v i
no goals