Theorem: LO.FirstOrder.Arith.FirstIncompleteness.codeAux_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 n✝ : ℕ
c : Code (n✝ + 1)
ih :
  ∀ {v : Fin (n✝ + 1) → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
v : Fin n✝ → M
z z' : M
h₁ :
  (Semiformula.Eval (standardModel M) ![] (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z :> v) i))
    (codeAux c)
hm₁ : ∀ x < z, ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)
h₂ :
  (Semiformula.Eval (standardModel M) ![] (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z' :> v) i))
    (codeAux c)
hm₂ : ∀ x < z', ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)
hz : ¬z = z'
Hz :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {n : ℕ} (c : Code (n + 1)),
    (∀ {v : Fin (n + 1) → M} {z z' : M},
        (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z') →
      ∀ {v : Fin n → M} {z z' : M},
        (Semiformula.Eval (standardModel M) ![] (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z :> v) i))
            (codeAux c) →
          (∀ x < z, ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)) →
            (Semiformula.Eval (standardModel M) ![]
                  (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z' :> v) i))
                (codeAux c) →
              (∀ x < z',
                  ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)) →
                ¬z = z' → z < z' → False
h : ¬z < z'
⊢ False
Tactic:
have : z' < z := lt_of_le_of_ne (not_lt.mp h) (Ne.symm hz)
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 n✝ : ℕ
c : Code (n✝ + 1)
ih :
  ∀ {v : Fin (n✝ + 1) → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
v : Fin n✝ → M
z z' : M
h₁ :
  (Semiformula.Eval (standardModel M) ![] (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z :> v) i))
    (codeAux c)
hm₁ : ∀ x < z, ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)
h₂ :
  (Semiformula.Eval (standardModel M) ![] (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z' :> v) i))
    (codeAux c)
hm₂ : ∀ x < z', ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)
hz : ¬z = z'
Hz :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] {k : ℕ} {n : ℕ} (c : Code (n + 1)),
    (∀ {v : Fin (n + 1) → M} {z z' : M},
        (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z') →
      ∀ {v : Fin n → M} {z z' : M},
        (Semiformula.Eval (standardModel M) ![] (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z :> v) i))
            (codeAux c) →
          (∀ x < z, ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)) →
            (Semiformula.Eval (standardModel M) ![]
                  (Semiterm.Operator.val (goedelNumber 0) ![] :> fun i => (z' :> v) i))
                (codeAux c) →
              (∀ x < z',
                  ∃ x_1, ¬x_1 = 0 ∧ (Semiformula.Eval (standardModel M) ![] (x_1 :> x :> fun i => v i)) (codeAux c)) →
                ¬z = z' → z < z' → False
h : ¬z < z'
this : z' < z
⊢ False