internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.code_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k : ℕ
c : Code k
v : Fin k → M
z z' : M
⊢ (Semiformula.Evalbm M (z :> v)) (code c) → (Semiformula.Evalbm M (z' :> v)) (code c) → z = z'
Tactic:
simp[code, Semiformula.eval_rew, Matrix.empty_eq, Function.comp, Matrix.comp_vecCons']
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k : ℕ
c : Code k
v : Fin k → M
z z' : M
⊢ (Semiformula.Eval (standardModel M) ![] fun x => (z :> v) x) (codeAux c) →
    (Semiformula.Eval (standardModel M) ![] fun x => (z' :> v) x) (codeAux c) → z = z'
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.code_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k : ℕ
c : Code k
v : Fin k → M
z z' : M
⊢ (Semiformula.Eval (standardModel M) ![] fun x => (z :> v) x) (codeAux c) →
    (Semiformula.Eval (standardModel M) ![] fun x => (z' :> v) x) (codeAux c) → z = z'
Tactic:
exact codeAux_uniq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one
Proof state before:
k : ℕ
c : Code k
⊢ Hierarchy 𝚺 1 (codeAux c)
Tactic:
induction c <;> simp[codeAux, Matrix.fun_eq_vec₂]
Proof state after:
case comp
k m✝ n✝ : ℕ
a✝¹ : Code n✝
a✝ : Fin n✝ → Code m✝
a_ih✝¹ : Hierarchy 𝚺 1 (codeAux a✝¹)
a_ih✝ : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (a✝ a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))

case rfind
k n✝ : ℕ
a✝ : Code (n✝ + 1)
a_ih✝ : Hierarchy 𝚺 1 (codeAux a✝)
⊢ Hierarchy 𝚺 1 (codeAux a✝) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))))”)
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one
Proof state before:
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
Tactic:
case comp c d ihc ihg =>
  exact Hierarchy.exClosure (by simp [ihc, ihg])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one
Proof state before:
k✝ k : ℕ
c : Code (k + 1)
ih : Hierarchy 𝚺 1 (codeAux c)
⊢ Hierarchy 𝚺 1 (codeAux c) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))))”)
Tactic:
case rfind k c ih => simp [ih]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one
Proof state before:
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 1
    (∃*
      (Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
        Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
Tactic:
exact Hierarchy.exClosure (by simp [ihc, ihg])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one
Proof state before:
k m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
ihc : Hierarchy 𝚺 1 (codeAux c)
ihg : ∀ (a : Fin n✝), Hierarchy 𝚺 1 (codeAux (d a))
⊢ Hierarchy 𝚺 (0 + 1)
    ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c) ⋏
      Matrix.conj fun i => (Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))
Tactic:
simp [ihc, ihg]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_sigma_one
Proof state before:
k✝ k : ℕ
c : Code (k + 1)
ih : Hierarchy 𝚺 1 (codeAux c)
⊢ Hierarchy 𝚺 1 (codeAux c) ∧
    Hierarchy 𝚺 1
      (“(∀[!!(![#0, &0] 0) < !!(![#0, &0] 1)]
            ∃'
              (¬!!(![#0, ‘0’] 0) = !!(![#0, ‘0’] 1) ∧
                  !((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))))”)
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.natCast_nat
Proof state before:
n : ℕ
⊢ ↑n = n
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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']
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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
Proof 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))
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.FirstIncompleteness.models_codeAux
Proof 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
Proof 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))