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 : α
b : β
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Tactic:
let f' : Vector ℕ 2 → ℕ := fun v =>
  Option.get! ((decode v.head).bind fun x => (decode v.tail.head).map fun y => (encode $ f x y))
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 : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)

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 : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Tactic:
have : Nat.Partrec' (f' : Vector ℕ 2 →. ℕ) :=
  Nat.Partrec'.part_iff.mpr <| Computable.partrec <|
      (Primrec.option_get!).to_comp.comp <|
        Computable.option_bind
          (Computable.decode.comp .vector_head) <|
            Computable.option_map
              (Computable.decode.comp $ Computable.vector_head.comp $ Computable.vector_tail.comp .fst) <|
                Computable.encode.comp₂ <| hf.comp₂ (Computable.snd.comp₂ .left) .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 : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)

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 : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
Tactic:
simpa [f', Matrix.comp_vecCons' (fun x : ℕ => (⸢x⸣ : Semiterm ℒₒᵣ Empty 1)),
  Matrix.constant_eq_singleton, graphTotal₂] using
    provable_computable_code_uniq T this ![encode a, encode b]
State after:
no goals