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

State before:
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode f = encode fun i => encode (f i)
Tactic:
simp[encode_finArrow, encode_list (List.ofFn f)]
State after:
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode ∘ f = fun i => encode (f i)

State before:
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode ∘ f = fun i => encode (f i)
Tactic:
funext i
State after:
case h
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
i : Fin k
⊢ (encode ∘ f) i = encode (f i)

State before:
case h
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
i : Fin k
⊢ (encode ∘ f) i = encode (f i)
Tactic:
simp
State after:
no goals