Theorem: LO.FirstOrder.Arith.standardModel_unique' (Logic/FirstOrder/Arith/Model.lean)

State before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.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:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.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:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.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:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.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:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
r : ℒₒᵣ.Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(=) x✝ = Structure.rel op(=) x✝
Tactic:
simp
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
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
r : ℒₒᵣ.Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(<) x✝ = Structure.rel op(<) x✝
Tactic:
simp
State after:
no goals