Theorem: LO.FirstOrder.Arith.FirstIncompleteness.representation (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 : Partrec f
x : α
y : σ
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Tactic:
let f' : Vector ℕ 1 →. ℕ := fun x => Part.bind (decode (α := α) x.head) fun a => (f a).map encode
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 : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x

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 : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Tactic:
have : Nat.Partrec' f' :=
  Nat.Partrec'.part_iff.mpr
    (Partrec.bind (Computable.ofOption $ Primrec.to_comp $ Primrec.decode.comp Primrec.vector_head)
    (Partrec.to₂ <| Partrec.map (hf.comp .snd) (Computable.encode.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 : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
this : Nat.Partrec' f'
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x

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 : Partrec f
x : α
y : σ
f' : Vector ℕ 1 →. ℕ := fun x => (↑(decode x.head)).bind fun a => Part.map encode (f a)
this : Nat.Partrec' f'
⊢ T ⊢! [→ ⸢y⸣, ⸢x⸣].hom (graph f) ↔ y ∈ f x
Tactic:
simpa [f', Matrix.constant_eq_singleton] using
  provable_iff_mem_partrec this (y := encode y) (v := ![encode x])
State after:
no goals