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

State before:
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
s : Structure ℒₒᵣ M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
rcases standardModel_unique M s
State after:
case refl
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ

State before:
case refl
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
exact H M
State after:
no goals