Theorem: LO.FirstOrder.Arith.standardModelExp_unique' (Logic/FirstOrder/Arith/EA/Basic.lean)

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 0 → M
⊢ Structure.func Language.Zero.zero x✝ = Structure.func Language.Zero.zero x✝
Tactic:
simp[Matrix.empty_eq]
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 0 → M
⊢ Structure.func Language.One.one x✝ = Structure.func Language.One.one x✝
Tactic:
simp[Matrix.empty_eq]
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 2 → M
⊢ Structure.func Language.Add.add x✝ = Structure.func Language.Add.add x✝
Tactic:
simp
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 2 → M
⊢ Structure.func Language.Mul.mul x✝ = Structure.func Language.Mul.mul x✝
Tactic:
simp
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
f : ℒₒᵣ(exp).Func k
x✝ : Fin 1 → M
⊢ Structure.func Language.Exp.exp x✝ = Structure.func Language.Exp.exp x✝
Tactic:
simp
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
r : ℒₒᵣ(exp).Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(=) x✝ = Structure.rel op(=) x✝
Tactic:
simp
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ(exp) M
hZero : Structure.Zero ℒₒᵣ(exp) M
hOne : Structure.One ℒₒᵣ(exp) M
hAdd : Structure.Add ℒₒᵣ(exp) M
hMul : Structure.Mul ℒₒᵣ(exp) M
hExp : Structure.Exp ℒₒᵣ(exp) M
hEq : Structure.Eq ℒₒᵣ(exp) M
hLT : Structure.LT ℒₒᵣ(exp) M
k : ℕ
r : ℒₒᵣ(exp).Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(<) x✝ = Structure.rel op(<) x✝
Tactic:
simp
State after:
no goals