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

State before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
hf : Computable f
a : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)
Tactic:
have : Nat.Partrec' (f' : Vector ℕ 1 →. ℕ) :=
  Nat.Partrec'.part_iff.mpr <| Computable.partrec <|
      (Primrec.option_get!).to_comp.comp <|
        Computable.option_map
          (Computable.decode.comp .vector_head) <|
            Computable.encode.comp₂ <| hf.comp₂ .right
State after:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
hf : Computable f
a : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)

State before:
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
hf : Computable f
a : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)
Tactic:
simpa [f', Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
  provable_computable_code_uniq T this ![encode a]
State after:
no goals