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

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
hc : c.eval f
y : ℕ
v : Fin k → ℕ
⊢ (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
Tactic:
induction hc generalizing y <;> simp [code, codeAux, models_iff]
State after:
case zero
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 0 ↔ 0 = Part.some y

case one
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 1 ↔ 1 = Part.some y

case add
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ + v j✝ ↔ v i✝ + v j✝ = y

case mul
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ * v j✝ ↔ v i✝ * v j✝ = y

case proj
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ ↔ v i✝ = y

case equal
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i✝ = v j✝ ∧ y = 1 ∨ ¬v i✝ = v j✝ ∧ y = 0 ↔ (v i✝).isEqNat (v j✝) = y

case lt
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i✝ < v j✝ ∧ y = 1 ∨ v j✝ ≤ v i✝ ∧ y = 0 ↔ (v i✝).isLtNat (v j✝) = y

case comp
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c✝ : Code n✝
d✝ : Fin n✝ → Code m✝
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c✝.eval f✝
a✝ : ∀ (i : Fin n✝), (d✝ i).eval (g✝ i)
a_ih✝¹ : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c✝) ↔ f✝ (Vector.ofFn v) = Part.some y
a_ih✝ :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d✝ i)) ↔ g✝ i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) e (y :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c✝)) ∧
        ∀ (i : Fin n✝),
          (Semiformula.Eval (standardModel ℕ) e (y :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d✝ i)))) ↔
    (Vector.mOfFn fun i => g✝ i (Vector.ofFn v)).bind f✝ = Part.some y

case rfind
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
c✝ : Code (n✝ + 1)
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : c✝.eval ↑f✝
a_ih✝ :
  ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c✝) ↔ ↑f✝ (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ ((Semiformula.Evalfm ℕ (y :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c✝)) ∧
      ∀ x < y,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel ℕ) ![x_1, x] (y :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c✝))) ↔
    (Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 0 ↔ 0 = Part.some y
Tactic:
case zero =>
  have : (0 : Part ℕ) = Part.some 0 := rfl
  simp[this, eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 1 ↔ 1 = Part.some y
Tactic:
case one =>
  have : (1 : Part ℕ) = Part.some 1 := rfl
  simp[this, eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i = v j ∧ y = 1 ∨ ¬v i = v j ∧ y = 0 ↔ (v i).isEqNat (v j) = y
Tactic:
case equal i j =>
  by_cases hv : v i = v j <;> simp[hv, Nat.isEqNat, eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ + v j✝ ↔ v i✝ + v j✝ = y
Tactic:
case add => simp[eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ * v j✝ ↔ v i✝ * v j✝ = y
Tactic:
case mul => simp[eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ ↔ v i✝ = y
Tactic:
case proj => simp[eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 0 ↔ 0 = Part.some y
Tactic:
have : (0 : Part ℕ) = Part.some 0 := rfl
State after:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
this : 0 = Part.some 0
⊢ y = 0 ↔ 0 = Part.some y

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
this : 0 = Part.some 0
⊢ y = 0 ↔ 0 = Part.some y
Tactic:
simp[this, eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
⊢ y = 1 ↔ 1 = Part.some y
Tactic:
have : (1 : Part ℕ) = Part.some 1 := rfl
State after:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
this : 1 = Part.some 1
⊢ y = 1 ↔ 1 = Part.some y

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ y : ℕ
v : Fin n✝ → ℕ
this : 1 = Part.some 1
⊢ y = 1 ↔ 1 = Part.some y
Tactic:
simp[this, eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i = v j ∧ y = 1 ∨ ¬v i = v j ∧ y = 0 ↔ (v i).isEqNat (v j) = y
Tactic:
by_cases hv : v i = v j <;> simp[hv, Nat.isEqNat, eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i < v j ∧ y = 1 ∨ v j ≤ v i ∧ y = 0 ↔ (v i).isLtNat (v j) = y
Tactic:
by_cases hv : v i < v j <;> simp[hv, Nat.isLtNat, eq_comm]
State after:
case neg
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
hv : ¬v i < v j
⊢ y = 0 → v j ≤ v i

State before:
case neg
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
hv : ¬v i < v j
⊢ y = 0 → v j ≤ v i
Tactic:
simp [Nat.not_lt.mp hv]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ + v j✝ ↔ v i✝ + v j✝ = y
Tactic:
simp[eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ * v j✝ ↔ v i✝ * v j✝ = y
Tactic:
simp[eq_comm]
State after:
no goals

State before:
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i✝ : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ y = v i✝ ↔ v i✝ = y
Tactic:
simp[eq_comm]
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) e (y :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) ∧
        ∀ (i : Fin n✝),
          (Semiformula.Eval (standardModel ℕ) e (y :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) ↔
    (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
Tactic:
simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
State after:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
        ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))) ↔
    (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
        ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))) ↔
    (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
Tactic:
constructor
State after:
case mp
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
        ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))) →
    (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y

case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y →
    ∃ e,
      (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
        ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))

State before:
case mp
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (∃ e,
      (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
        ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))) →
    (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
Tactic:
rintro ⟨e, hf, hg⟩
State after:
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y

State before:
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
Tactic:
have hf : f (Vector.ofFn e) = Part.some y := (ihf _ _).mp hf
State after:
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf✝ : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
hf : f (Vector.ofFn e) = Part.some y
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y

State before:
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf✝ : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
hf : f (Vector.ofFn e) = Part.some y
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
Tactic:
have hg : ∀ i, g i (Vector.ofFn v) = Part.some (e i) := fun i => (ihg i _ _).mp (hg i)
State after:
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf✝ : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg✝ : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
hf : f (Vector.ofFn e) = Part.some y
hg : ∀ (i : Fin n✝), g i (Vector.ofFn v) = Part.some (e i)
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y

State before:
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf✝ : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg✝ : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
hf : f (Vector.ofFn e) = Part.some y
hg : ∀ (i : Fin n✝), g i (Vector.ofFn v) = Part.some (e i)
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
Tactic:
simp[hg, hf]
State after:
no goals

State before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y →
    ∃ e,
      (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
        ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
intro h
State after:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))

State before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
have : ∃ w, (∀ i, Vector.get w i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w := by
  simpa using Part.eq_some_iff.mp h
State after:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
this : ∃ w, (∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))

State before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
this : ∃ w, (∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
rcases this with ⟨w, hw, hy⟩
State after:
case mpr.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))

State before:
case mpr.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
⊢ ∃ e,
    (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c) ∧
      ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
Tactic:
exact ⟨w.get, (ihf y w.get).mpr (by simpa[Part.eq_some_iff] using hy),
  fun i => (ihg i (w.get i) v).mpr (by simpa[Part.eq_some_iff] using hw i)⟩
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
⊢ ∃ w, (∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w
Tactic:
simpa using Part.eq_some_iff.mp h
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
⊢ f (Vector.ofFn w.get) = Part.some y
Tactic:
simpa[Part.eq_some_iff] using hy
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
h : (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
w : Vector ℕ n✝
hw : ∀ (i : Fin n✝), w.get i ∈ g i (Vector.ofFn v)
hy : y ∈ f w
i : Fin n✝
⊢ g i (Vector.ofFn v) = Part.some (w.get i)
Tactic:
simpa[Part.eq_some_iff] using hw i
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ ((Semiformula.Evalfm ℕ (y :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) ∧
      ∀ x < y,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel ℕ) ![x_1, x] (y :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) ↔
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons', ihf, Vector.ofFn_vecCons]
State after:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) ↔
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) ↔
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
constructor
State after:
case mp
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) →
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y

case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y →
    f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0

State before:
case mp
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0) →
    (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
rintro ⟨hy, h⟩
State after:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y

State before:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
Tactic:
simp[Part.eq_some_iff]
State after:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ f (y ::ᵥ Vector.ofFn v) = 0 ∧ ∀ {m : ℕ}, m < y → ¬f (m ::ᵥ Vector.ofFn v) = 0

State before:
case mp.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ f (y ::ᵥ Vector.ofFn v) = 0 ∧ ∀ {m : ℕ}, m < y → ¬f (m ::ᵥ Vector.ofFn v) = 0
Tactic:
exact ⟨by simpa using hy, by intro z hz; simpa using h z hz⟩
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ f (y ::ᵥ Vector.ofFn v) = 0
Tactic:
simpa using hy
State after:
no goals

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
⊢ ∀ {m : ℕ}, m < y → ¬f (m ::ᵥ Vector.ofFn v) = 0
Tactic:
intro z hz
State after:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
z : ℕ
hz : z < y
⊢ ¬f (z ::ᵥ Vector.ofFn v) = 0

State before:
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
hy : f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![]
h : ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
z : ℕ
hz : z < y
⊢ ¬f (z ::ᵥ Vector.ofFn v) = 0
Tactic:
simpa using h z hz
State after:
no goals

State before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
⊢ (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y →
    f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
      ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
Tactic:
intro h
State after:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
h : (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
⊢ f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
    ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0

State before:
case mpr
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
n✝ : ℕ
c : Code (n✝ + 1)
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : c.eval ↑f
ihf : ∀ (y : ℕ) (v : Fin (n✝ + 1) → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ ↑f (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin n✝ → ℕ
h : (Nat.rfind fun n => Part.some (decide (f (n ::ᵥ Vector.ofFn v) = 0))) = Part.some y
⊢ f (y ::ᵥ Vector.ofFn v) = Semiterm.Operator.val (goedelNumber 0) ![] ∧
    ∀ x < y, ¬f (x ::ᵥ Vector.ofFn fun i => v i) = 0
Tactic:
simpa using Nat.mem_rfind.mp (Part.eq_some_iff.mp h)
State after:
no goals