rcases hk with rfl
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
i : ι
k : ℕ
hk : Fintype.card ι = k
v : Fin k → α
⊢ (fintypeArrowEquivFinArrow' hk).symm v i = v (Fin.cast hk (fintypeEquivFin i))
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
i : ι
v : Fin (Fintype.card ι) → α
⊢ (fintypeArrowEquivFinArrow' ⋯).symm v i = v (Fin.cast ⋯ (fintypeEquivFin i))