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

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]
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

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
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

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
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

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

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]
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

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
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

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