internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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 _
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.val_lMap_oringEmb
Proof state before:
n : ℕ
ξ : Type u_2
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
e : Fin n → M
ε : ξ → M
t : Semiterm ℒₒᵣ ξ n
⊢ Semiterm.valm M e ε (Semiterm.lMap oringEmb t) = Semiterm.valm M e ε t
Tactic:
simp [Semiterm.val_lMap, standardModel_lMap_oringEmb_eq_standardModel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.eval_lMap_oringEmb
Proof state before:
n : ℕ
ξ : Type u_2
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
e : Fin n → M
ε : ξ → M
p : Semiformula ℒₒᵣ ξ n
⊢ (Semiformula.Evalm M e ε) ((Semiformula.lMap oringEmb) p) ↔ (Semiformula.Evalm M e ε) p
Tactic:
simp [Semiformula.eval_lMap, standardModel_lMap_oringEmb_eq_standardModel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ M ⊧ₘ* Theory.lMap oringEmb T ↔ M ⊧ₘ* T
Tactic:
simp [modelsTheory_iff]
Proof state after:
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p) ↔ ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p) ↔ ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p
Tactic:
constructor
Proof state after:
case mp
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p) → ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p

case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p) → ∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
case mp
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p) → ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p
Tactic:
intro H p hp
Proof state after:
case mp
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
H : ∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p
p : Sentence ℒₒᵣ
hp : p ∈ T
⊢ M ⊧ₘ p
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
case mp
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
H : ∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p
p : Sentence ℒₒᵣ
hp : p ∈ T
⊢ M ⊧ₘ p
Tactic:
exact eval_lMap_oringEmb.mp <| @H (Semiformula.lMap oringEmb p) (Set.mem_image_of_mem _ hp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p) → ∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p
Tactic:
simp [Theory.lMap]
Proof state after:
case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p) → ∀ a ∈ T, M ⊧ₘ (Semiformula.lMap oringEmb) a
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p) → ∀ a ∈ T, M ⊧ₘ (Semiformula.lMap oringEmb) a
Tactic:
intro H p hp
Proof state after:
case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
H : ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p
p : Semiformula ℒₒᵣ Empty 0
hp : p ∈ T
⊢ M ⊧ₘ (Semiformula.lMap oringEmb) p
Theorem: LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb
Proof state before:
case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
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
T : Theory ℒₒᵣ
H : ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p
p : Semiformula ℒₒᵣ Empty 0
hp : p ∈ T
⊢ M ⊧ₘ (Semiformula.lMap oringEmb) p
Tactic:
exact eval_lMap_oringEmb.mpr (H hp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Standard.models_succInd
Proof state before:
n : ℕ
μ : Type v
e : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
⊢ ℕ ⊧ₘ ∀ᶠ* succInd p
Tactic:
simp[Empty.eq_elim, succInd, models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons',
  Semiformula.eval_substs, Semiformula.eval_rew_q Rew.toS, Function.comp]
Proof state after:
n : ℕ
μ : Type v
e : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModel ℕ) ![0] ε) p →
      (∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] ε) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] ε) p
Theorem: LO.FirstOrder.Arith.Standard.models_succInd
Proof state before:
n : ℕ
μ : Type v
e : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModel ℕ) ![0] ε) p →
      (∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] ε) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] ε) p
Tactic:
intro e hzero hsucc x
Proof state after:
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
x : ℕ
⊢ (Semiformula.Eval (standardModel ℕ) ![x] e) p