Theorem: LO.FirstOrder.Arith.FirstIncompleteness.code_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.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']
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'

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
State after:
no goals