Theorem: Primrec.finArrow_app (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
n : ℕ
v : σ → Fin n → α
f : σ → Fin n
hv : Primrec v
hf : Primrec f
this : Primrec fun x => (List.ofFn (v x)).get? ↑(f x)
x : σ
⊢ (List.ofFn (v x)).get? ↑(f x) = some (v x (f x))
Tactic:
simp[List.ofFnNthVal]
State after:
no goals