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

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = encode fun i => encode (f i)
Tactic:
simp[encode_fintypeArrow, encode_finArrow, encode_list (List.ofFn $ fintypeArrowEquivFinArrow f)]
State after:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode ∘ fintypeArrowEquivFinArrow f = fintypeArrowEquivFinArrow fun i => encode (f i)

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode ∘ fintypeArrowEquivFinArrow f = fintypeArrowEquivFinArrow fun i => encode (f i)
Tactic:
funext i
State after:
case h
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : Fin (Fintype.card ι)
⊢ (encode ∘ fintypeArrowEquivFinArrow f) i = fintypeArrowEquivFinArrow (fun i => encode (f i)) i

State before:
case h
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
i : Fin (Fintype.card ι)
⊢ (encode ∘ fintypeArrowEquivFinArrow f) i = fintypeArrowEquivFinArrow (fun i => encode (f i)) i
Tactic:
simp
State after:
no goals