Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel (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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.lMap oringEmb s = standardModel M
Tactic:
apply standardModel_unique' M _
State after:
case hZero
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Zero ℒₒᵣ M

case hOne
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.One ℒₒᵣ M

case hAdd
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Add ℒₒᵣ M

case hMul
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Mul ℒₒᵣ M

case hEq
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Eq ℒₒᵣ M

case hLT
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.LT ℒₒᵣ M

State before:
case hZero
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Zero ℒₒᵣ M
Tactic:
exact @Structure.Zero.mk ℒₒᵣ M (s.lMap Language.oringEmb) _ _ (by simp [Semiterm.Operator.val, ←Semiterm.val_lMap]; exact Structure.Zero.zero)
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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Semiterm.Operator.val op(0) ![] = 0
Tactic:
simp [Semiterm.Operator.val, ←Semiterm.val_lMap]
State after:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Semiterm.val s ![] Empty.elim op(0).term = 0

State before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Semiterm.val s ![] Empty.elim op(0).term = 0
Tactic:
exact Structure.Zero.zero
State after:
no goals

State before:
case hOne
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.One ℒₒᵣ M
Tactic:
exact @Structure.One.mk ℒₒᵣ M (s.lMap Language.oringEmb) _ _ (by simp [Semiterm.Operator.val, ←Semiterm.val_lMap]; exact Structure.One.one)
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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Semiterm.Operator.val op(1) ![] = 1
Tactic:
simp [Semiterm.Operator.val, ←Semiterm.val_lMap]
State after:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Semiterm.val s ![] Empty.elim op(1).term = 1

State before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Semiterm.val s ![] Empty.elim op(1).term = 1
Tactic:
exact Structure.One.one
State after:
no goals

State before:
case hAdd
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Add ℒₒᵣ M
Tactic:
exact @Structure.Add.mk ℒₒᵣ M (s.lMap Language.oringEmb) _ _ (fun a b ↦ by simp [Semiterm.Operator.val, ←Semiterm.val_lMap]; exact Structure.Add.add a b)
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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ op(+).val ![a, b] = a + b
Tactic:
simp [Semiterm.Operator.val, ←Semiterm.val_lMap]
State after:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ Semiterm.val s ![a, b] Empty.elim op(+).term = a + b

State before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ Semiterm.val s ![a, b] Empty.elim op(+).term = a + b
Tactic:
exact Structure.Add.add a b
State after:
no goals

State before:
case hMul
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Mul ℒₒᵣ M
Tactic:
exact @Structure.Mul.mk ℒₒᵣ M (s.lMap Language.oringEmb) _ _ (fun a b ↦ by simp [Semiterm.Operator.val, ←Semiterm.val_lMap]; exact Structure.Mul.mul a b)
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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ op(*).val ![a, b] = a * b
Tactic:
simp [Semiterm.Operator.val, ←Semiterm.val_lMap]
State after:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ Semiterm.val s ![a, b] Empty.elim op(*).term = a * b

State before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ Semiterm.val s ![a, b] Empty.elim op(*).term = a * b
Tactic:
exact Structure.Mul.mul a b
State after:
no goals

State before:
case hEq
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.Eq ℒₒᵣ M
Tactic:
exact @Structure.Eq.mk ℒₒᵣ M (s.lMap Language.oringEmb) _ (fun a b ↦ by
  simp [Semiformula.Operator.val, ←Semiformula.eval_lMap]; exact Structure.Eq.eq a b)
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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ op(=).val ![a, b] ↔ a = b
Tactic:
simp [Semiformula.Operator.val, ←Semiformula.eval_lMap]
State after:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ (Semiformula.Eval s ![a, b] Empty.elim) op(=).sentence ↔ a = b

State before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ (Semiformula.Eval s ![a, b] Empty.elim) op(=).sentence ↔ a = b
Tactic:
exact Structure.Eq.eq a b
State after:
no goals

State before:
case hLT
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
⊢ Structure.LT ℒₒᵣ M
Tactic:
exact @Structure.LT.mk ℒₒᵣ M (s.lMap Language.oringEmb) _ _ (fun a b ↦ by
  simp [Semiformula.Operator.val, ←Semiformula.eval_lMap]; exact Structure.LT.lt a b)
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
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ op(<).val ![a, b] ↔ a < b
Tactic:
simp [Semiformula.Operator.val, ←Semiformula.eval_lMap]
State after:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ (Semiformula.Eval s ![a, b] Empty.elim) op(<).sentence ↔ a < b

State before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ (Semiformula.Eval s ![a, b] Empty.elim) op(<).sentence ↔ a < b
Tactic:
exact Structure.LT.lt a b
State after:
no goals