Theorem: Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin (Logic/Vorspiel/Computability.lean)

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : Fin (Fintype.card ι) → α
⊢ (fintypeArrowEquivFinArrow fun i => f (fintypeEquivFin i)) = f
Tactic:
funext i
State after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : Fin (Fintype.card ι) → α
i : Fin (Fintype.card ι)
⊢ fintypeArrowEquivFinArrow (fun i => f (fintypeEquivFin i)) i = f i

State before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : Fin (Fintype.card ι) → α
i : Fin (Fintype.card ι)
⊢ fintypeArrowEquivFinArrow (fun i => f (fintypeEquivFin i)) i = f i
Tactic:
simp
State after:
no goals