Theorem: Nat.ArithPart₁.exists_code (Logic/Vorspiel/Arith.lean)

State before:
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Tactic:
rcases exists_code hf with ⟨cf, hcf⟩
State after:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f

State before:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Tactic:
choose cg hcg using fun i            => exists_code (hg i)
State after:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
cg : Fin n✝ → Code n✝¹
hcg : ∀ (i : Fin n✝), (cg i).eval (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f

State before:
case intro
n✝¹ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ n✝¹ →. ℕ
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
cf : Code n✝
hcf : cf.eval f
cg : Fin n✝ → Code n✝¹
hcg : ∀ (i : Fin n✝), (cg i).eval (g i)
⊢ ∃ c, c.eval fun v => (mOfFn fun i => g i v) >>= f
Tactic:
exact ⟨cf.comp cg, Code.eval.comp cf cg f g hcf hcg⟩
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
rcases exists_code hf with ⟨cf, hcf⟩
State after:
case intro
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
cf : Code (n✝ + 1)
hcf : cf.eval ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))

State before:
case intro
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
hf : ArithPart₁ ↑f
cf : Code (n✝ + 1)
hcf : cf.eval ↑f
⊢ ∃ c, c.eval fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
exact ⟨cf.rfind, Code.eval.rfind cf f hcf⟩
State after:
no goals