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

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.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
Tactic:
induction c generalizing z z' <;> simp[code, codeAux]
State after:
case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 0 → z' = 0 → z = z'

case one
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 1 → z' = 1 → z = z'

case add
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ + v j✝ → z' = v i✝ + v j✝ → z = z'

case mul
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ * v j✝ → z' = v i✝ * v j✝ → z = z'

case proj
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ → z' = v i✝ → z = z'

case equal
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i✝ = v j✝ ∧ z = 1 ∨ ¬v i✝ = v j✝ ∧ z = 0 → v i✝ = v j✝ ∧ z' = 1 ∨ ¬v i✝ = v j✝ ∧ z' = 0 → z = z'

case lt
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i✝ < v j✝ ∧ z = 1 ∨ v j✝ ≤ v i✝ ∧ z = 0 → v i✝ < v j✝ ∧ z' = 1 ∨ v j✝ ≤ v i✝ ∧ z' = 0 → z = z'

case comp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m✝ n✝ : ℕ
a✝¹ : Code n✝
a✝ : Fin n✝ → Code m✝
a_ih✝¹ :
  ∀ {v : Fin n✝ → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux a✝¹) → (Semiformula.Evalfm M (z' :> v)) (codeAux a✝¹) → z = z'
a_ih✝ :
  ∀ (a : Fin n✝) {v : Fin m✝ → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (a✝ a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (a✝ a)) → z = z'
v : Fin m✝ → M
z z' : M
⊢ ∀ (x : Fin n✝ → M),
    (Semiformula.Eval (standardModel M) x (z :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹)) →
      (∀ (i : Fin n✝),
          (Semiformula.Eval (standardModel M) x (z :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))) →
        ∀ (x : Fin n✝ → M),
          (Semiformula.Eval (standardModel M) x (z' :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux a✝¹)) →
            (∀ (i : Fin n✝),
                (Semiformula.Eval (standardModel M) x (z' :> v))
                  ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (a✝ i)))) →
              z = z'

case rfind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
a✝ : Code (n✝ + 1)
a_ih✝ :
  ∀ {v : Fin (n✝ + 1) → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux a✝) → (Semiformula.Evalfm M (z' :> v)) (codeAux a✝) → z = z'
v : Fin n✝ → M
z z' : M
⊢ (Semiformula.Evalfm M (z :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux a✝)) →
    (∀ x < z,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel M) ![x_1, x] (z :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))) →
      (Semiformula.Evalfm M (z' :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux a✝)) →
        (∀ x < z',
            ∃ x_1,
              ¬x_1 = 0 ∧
                (Semiformula.Eval (standardModel M) ![x_1, x] (z' :> v))
                  ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux a✝))) →
          z = z'

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✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 0 → z' = 0 → z = z'
Tactic:
case zero => rintro rfl rfl; rfl
State after:
no goals

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✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 1 → z' = 1 → z = z'
Tactic:
case one  => rintro rfl rfl; rfl
State after:
no goals

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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ + v j✝ → z' = v i✝ + v j✝ → z = z'
Tactic:
case add  => rintro rfl rfl; rfl
State after:
no goals

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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ * v j✝ → z' = v i✝ * v j✝ → z = z'
Tactic:
case mul  => rintro rfl rfl; rfl
State after:
no goals

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✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ → z' = v i✝ → z = z'
Tactic:
case proj => rintro rfl rfl; rfl
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) x (z :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
      (∀ (i : Fin n),
          (Semiformula.Eval (standardModel M) x (z :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) x (z' :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
            (∀ (i : Fin n),
                (Semiformula.Eval (standardModel M) x (z' :> v))
                  ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
              z = z'
Tactic:
case comp m n c d ihc ihd =>
  simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
  intro w₁ hc₁ hd₁ w₂ hc₂ hd₂;
  have : w₁ = w₂ := funext fun i => ihd i (hd₁ i) (hd₂ i)
  rcases this with rfl
  exact ihc hc₁ hc₂
State after:
no goals

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
⊢ (Semiformula.Evalfm M (z :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
    (∀ x < z,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel M) ![x_1, x] (z :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
      (Semiformula.Evalfm M (z' :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
        (∀ x < z',
            ∃ x_1,
              ¬x_1 = 0 ∧
                (Semiformula.Eval (standardModel M) ![x_1, x] (z' :> v))
                  ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
          z = z'
Tactic:
case rfind c ih =>
  simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
  intro h₁ hm₁ h₂ hm₂
  by_contra hz
  wlog h : z < z' with Hz
  case inr =>
    have : z' < z := lt_of_le_of_ne (not_lt.mp h) (Ne.symm hz)
    exact Hz (k := k) c ih h₂ hm₂ h₁ hm₁ (Ne.symm hz) this
  have : ∃ x, x ≠ 0 ∧ (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c) := hm₂ z h
  rcases this with ⟨x, xz, hx⟩
  exact xz (ih hx h₁)
State after:
no goals

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✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 0 → z' = 0 → z = z'
Tactic:
rintro rfl rfl
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✝ : ℕ
v : Fin n✝ → M
⊢ 0 = 0

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✝ : ℕ
v : Fin n✝ → M
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

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✝ : ℕ
v : Fin n✝ → M
z z' : M
⊢ z = 1 → z' = 1 → z = z'
Tactic:
rintro rfl rfl
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✝ : ℕ
v : Fin n✝ → M
⊢ 1 = 1

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✝ : ℕ
v : Fin n✝ → M
⊢ 1 = 1
Tactic:
rfl
State after:
no goals

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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ + v j✝ → z' = v i✝ + v j✝ → z = z'
Tactic:
rintro rfl rfl
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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ + v j✝ = v i✝ + v j✝

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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ + v j✝ = v i✝ + v j✝
Tactic:
rfl
State after:
no goals

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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ * v j✝ → z' = v i✝ * v j✝ → z = z'
Tactic:
rintro rfl rfl
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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ * v j✝ = v i✝ * v j✝

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✝ : ℕ
i✝ j✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ * v j✝ = v i✝ * v j✝
Tactic:
rfl
State after:
no goals

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✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ z = v i✝ → z' = v i✝ → z = z'
Tactic:
rintro rfl rfl
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✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ = v i✝

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✝ : ℕ
i✝ : Fin n✝
v : Fin n✝ → M
⊢ v i✝ = v i✝
Tactic:
rfl
State after:
no goals

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✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i = v j ∧ z = 1 ∨ ¬v i = v j ∧ z = 0 → v i = v j ∧ z' = 1 ∨ ¬v i = v j ∧ z' = 0 → z = z'
Tactic:
by_cases hv : v i = v j <;> simp[hv]
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i = v j
⊢ z = 1 → z' = 1 → z = z'

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i = v j
⊢ z = 0 → z' = 0 → z = z'

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i = v j
⊢ z = 1 → z' = 1 → z = z'
Tactic:
rintro rfl rfl
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i = v j
⊢ 1 = 1

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i = v j
⊢ 1 = 1
Tactic:
rfl
State after:
no goals

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i = v j
⊢ z = 0 → z' = 0 → z = z'
Tactic:
rintro rfl rfl
State after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i = v j
⊢ 0 = 0

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i = v j
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

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✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
⊢ v i < v j ∧ z = 1 ∨ v j ≤ v i ∧ z = 0 → v i < v j ∧ z' = 1 ∨ v j ≤ v i ∧ z' = 0 → z = z'
Tactic:
by_cases hv : v i < v j <;> simp[hv, -not_lt, ←not_lt]
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i < v j
⊢ z = 1 → z' = 1 → z = z'

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i < v j
⊢ z = 0 → z' = 0 → z = z'

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : v i < v j
⊢ z = 1 → z' = 1 → z = z'
Tactic:
rintro rfl rfl
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i < v j
⊢ 1 = 1

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : v i < v j
⊢ 1 = 1
Tactic:
rfl
State after:
no goals

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
z z' : M
hv : ¬v i < v j
⊢ z = 0 → z' = 0 → z = z'
Tactic:
rintro rfl rfl
State after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i < v j
⊢ 0 = 0

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k n✝ : ℕ
i j : Fin n✝
v : Fin n✝ → M
hv : ¬v i < v j
⊢ 0 = 0
Tactic:
rfl
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) x (z :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
      (∀ (i : Fin n),
          (Semiformula.Eval (standardModel M) x (z :> v))
            ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) x (z' :> v)) ((Rew.bind ![] (&0 :> fun x => #x)).hom (codeAux c)) →
            (∀ (i : Fin n),
                (Semiformula.Eval (standardModel M) x (z' :> v))
                  ((Rew.bind ![] (#i :> fun x => &x.succ)).hom (codeAux (d i)))) →
              z = z'
Tactic:
simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) ![] (z :> fun i => x i)) (codeAux c) →
      (∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (x i :> fun i => v i)) (codeAux (d i))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) ![] (z' :> fun i => x i)) (codeAux c) →
            (∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (x i :> fun i => v i)) (codeAux (d i))) → z = z'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
⊢ ∀ (x : Fin n → M),
    (Semiformula.Eval (standardModel M) ![] (z :> fun i => x i)) (codeAux c) →
      (∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (x i :> fun i => v i)) (codeAux (d i))) →
        ∀ (x : Fin n → M),
          (Semiformula.Eval (standardModel M) ![] (z' :> fun i => x i)) (codeAux c) →
            (∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (x i :> fun i => v i)) (codeAux (d i))) → z = z'
Tactic:
intro w₁ hc₁ hd₁ w₂ hc₂ hd₂
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
w₁ : Fin n → M
hc₁ : (Semiformula.Eval (standardModel M) ![] (z :> fun i => w₁ i)) (codeAux c)
hd₁ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
w₂ : Fin n → M
hc₂ : (Semiformula.Eval (standardModel M) ![] (z' :> fun i => w₂ i)) (codeAux c)
hd₂ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₂ i :> fun i => v i)) (codeAux (d i))
⊢ z = z'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
w₁ : Fin n → M
hc₁ : (Semiformula.Eval (standardModel M) ![] (z :> fun i => w₁ i)) (codeAux c)
hd₁ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
w₂ : Fin n → M
hc₂ : (Semiformula.Eval (standardModel M) ![] (z' :> fun i => w₂ i)) (codeAux c)
hd₂ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₂ i :> fun i => v i)) (codeAux (d i))
⊢ z = z'
Tactic:
have : w₁ = w₂ := funext fun i => ihd i (hd₁ i) (hd₂ i)
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
w₁ : Fin n → M
hc₁ : (Semiformula.Eval (standardModel M) ![] (z :> fun i => w₁ i)) (codeAux c)
hd₁ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
w₂ : Fin n → M
hc₂ : (Semiformula.Eval (standardModel M) ![] (z' :> fun i => w₂ i)) (codeAux c)
hd₂ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₂ i :> fun i => v i)) (codeAux (d i))
this : w₁ = w₂
⊢ z = z'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
w₁ : Fin n → M
hc₁ : (Semiformula.Eval (standardModel M) ![] (z :> fun i => w₁ i)) (codeAux c)
hd₁ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
w₂ : Fin n → M
hc₂ : (Semiformula.Eval (standardModel M) ![] (z' :> fun i => w₂ i)) (codeAux c)
hd₂ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₂ i :> fun i => v i)) (codeAux (d i))
this : w₁ = w₂
⊢ z = z'
Tactic:
rcases this with rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
w₁ : Fin n → M
hc₁ : (Semiformula.Eval (standardModel M) ![] (z :> fun i => w₁ i)) (codeAux c)
hd₁ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
hc₂ : (Semiformula.Eval (standardModel M) ![] (z' :> fun i => w₁ i)) (codeAux c)
hd₂ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
⊢ z = z'

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
k m n : ℕ
c : Code n
d : Fin n → Code m
ihc :
  ∀ {v : Fin n → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux c) → (Semiformula.Evalfm M (z' :> v)) (codeAux c) → z = z'
ihd :
  ∀ (a : Fin n) {v : Fin m → M} {z z' : M},
    (Semiformula.Evalfm M (z :> v)) (codeAux (d a)) → (Semiformula.Evalfm M (z' :> v)) (codeAux (d a)) → z = z'
v : Fin m → M
z z' : M
w₁ : Fin n → M
hc₁ : (Semiformula.Eval (standardModel M) ![] (z :> fun i => w₁ i)) (codeAux c)
hd₁ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
hc₂ : (Semiformula.Eval (standardModel M) ![] (z' :> fun i => w₁ i)) (codeAux c)
hd₂ : ∀ (i : Fin n), (Semiformula.Eval (standardModel M) ![] (w₁ i :> fun i => v i)) (codeAux (d i))
⊢ z = z'
Tactic:
exact ihc hc₁ hc₂
State after:
no goals

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
⊢ (Semiformula.Evalfm M (z :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
    (∀ x < z,
        ∃ x_1,
          ¬x_1 = 0 ∧
            (Semiformula.Eval (standardModel M) ![x_1, x] (z :> v))
              ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
      (Semiformula.Evalfm M (z' :> v)) ((Rew.bind ![] (⸢0⸣ :> Semiterm.fvar)).hom (codeAux c)) →
        (∀ x < z',
            ∃ x_1,
              ¬x_1 = 0 ∧
                (Semiformula.Eval (standardModel M) ![x_1, x] (z' :> v))
                  ((Rew.bind ![] (#0 :> #1 :> fun x => &x.succ)).hom (codeAux c))) →
          z = z'
Tactic:
simp[Semiformula.eval_rew, Function.comp, Matrix.empty_eq, Matrix.comp_vecCons']
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
⊢ (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'

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
⊢ (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'
Tactic:
intro h₁ hm₁ h₂ hm₂
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)
⊢ z = z'

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)
⊢ z = z'
Tactic:
by_contra hz
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'
⊢ False

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'
⊢ False
Tactic:
wlog h : z < z' with Hz
State after:
case inr
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

M✝ : Type u_1
inst✝¹⁰ : Zero M✝
inst✝⁹ : One M✝
inst✝⁸ : Add M✝
inst✝⁷ : Mul M✝
inst✝⁶ : LT M✝
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'
h : z < z'
⊢ False

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:
case inr =>
  have : z' < z := lt_of_le_of_ne (not_lt.mp h) (Ne.symm hz)
  exact Hz (k := k) c ih h₂ hm₂ h₁ hm₁ (Ne.symm hz) this
State after:
no goals

State before:
M✝ : Type u_1
inst✝¹⁰ : Zero M✝
inst✝⁹ : One M✝
inst✝⁸ : Add M✝
inst✝⁷ : Mul M✝
inst✝⁶ : LT M✝
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'
h : z < z'
⊢ False
Tactic:
have : ∃ x, x ≠ 0 ∧ (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c) := hm₂ z h
State after:
M✝ : Type u_1
inst✝¹⁰ : Zero M✝
inst✝⁹ : One M✝
inst✝⁸ : Add M✝
inst✝⁷ : Mul M✝
inst✝⁶ : LT M✝
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'
h : z < z'
this : ∃ x, x ≠ 0 ∧ (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c)
⊢ False

State before:
M✝ : Type u_1
inst✝¹⁰ : Zero M✝
inst✝⁹ : One M✝
inst✝⁸ : Add M✝
inst✝⁷ : Mul M✝
inst✝⁶ : LT M✝
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'
h : z < z'
this : ∃ x, x ≠ 0 ∧ (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c)
⊢ False
Tactic:
rcases this with ⟨x, xz, hx⟩
State after:
case intro.intro
M✝ : Type u_1
inst✝¹⁰ : Zero M✝
inst✝⁹ : One M✝
inst✝⁸ : Add M✝
inst✝⁷ : Mul M✝
inst✝⁶ : LT M✝
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'
h : z < z'
x : M
xz : x ≠ 0
hx : (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c)
⊢ False

State before:
case intro.intro
M✝ : Type u_1
inst✝¹⁰ : Zero M✝
inst✝⁹ : One M✝
inst✝⁸ : Add M✝
inst✝⁷ : Mul M✝
inst✝⁶ : LT M✝
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'
h : z < z'
x : M
xz : x ≠ 0
hx : (Semiformula.Evalfm M (x :> z :> fun i => v i)) (codeAux c)
⊢ False
Tactic:
exact xz (ih hx h₁)
State after:
no goals

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)
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

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'
this : z' < z
⊢ False
Tactic:
exact Hz (k := k) c ih h₂ hm₂ h₁ hm₁ (Ne.symm hz) this
State after:
no goals