Theorem: Encodable.fintypeArrowEquivFinArrow'_symm_app_fin_arrow (Logic/Vorspiel/Computability.lean)

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
k : ℕ
hk : Fintype.card (Fin k) = k
v : Fin k → α
⊢ (fintypeArrowEquivFinArrow' hk).symm v = v
Tactic:
funext i
State after:
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

State before:
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
Tactic:
simp[hk]
State after:
no goals