Theorem: LO.FirstOrder.Arith.FirstIncompleteness.provable_iff_computable (Logic/FirstOrder/Arith/Representation.lean)

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
⊢ f (Vector.ofFn v) ∈ ↑f (Vector.ofFn v)
Tactic:
simp
State after:
no goals