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

State before:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Tactic:
have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by
  rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩
  exact ⟨c, models_code hc⟩
State after:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
this : ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)

State before:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
this : ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
⊢ (Semiformula.Evalbm ℕ (y :> v)) (code (codeOfPartrec f)) ↔ y ∈ f (Vector.ofFn v)
Tactic:
exact Classical.epsilon_spec this y v
State after:
no goals

State before:
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
⊢ ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
Tactic:
rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩
State after:
case intro
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
c : Code k
hc : c.eval f
⊢ ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)

State before:
case intro
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
c : Code k
hc : c.eval f
⊢ ∃ c, ∀ (y : ℕ) (v : Fin k → ℕ), (Semiformula.Evalbm ℕ (y :> v)) (code c) ↔ y ∈ f (Vector.ofFn v)
Tactic:
exact ⟨c, models_code hc⟩
State after:
no goals