Theorem: LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic (Logic/FirstOrder/Arith/EA/Basic.lean)

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ℕ ⊧ₘ* 𝐄𝐀
Tactic:
simp [Theory.elementaryArithmetic, Theory.indScheme]
State after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ((∀ i ∈ 𝐏𝐀⁻, (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) i) ∧ ℕ ⊧ₘ* 𝐄𝐗𝐏) ∧
    ∀ (f : Sentence ℒₒᵣ(exp)) (x : Semiformula ℒₒᵣ(exp) ℕ 1),
      Hierarchy 𝚺 0 x → f = ∀ᶠ* succInd x → (standardModelExp ℕ).toStruc ⊧ f

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ((∀ i ∈ 𝐏𝐀⁻, (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) i) ∧ ℕ ⊧ₘ* 𝐄𝐗𝐏) ∧
    ∀ (f : Sentence ℒₒᵣ(exp)) (x : Semiformula ℒₒᵣ(exp) ℕ 1),
      Hierarchy 𝚺 0 x → f = ∀ᶠ* succInd x → (standardModelExp ℕ).toStruc ⊧ f
Tactic:
exact ⟨⟨by intro σ hσ; simpa [models_iff] using models_peanoMinus.realize hσ, models_exponential⟩,
  by rintro σ p _ rfl; exact modelsSuccInd_exp p⟩
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ∀ i ∈ 𝐏𝐀⁻, (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) i
Tactic:
intro σ hσ
State after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
σ : Semiformula ℒₒᵣ Empty 0
hσ : σ ∈ 𝐏𝐀⁻
⊢ (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) σ

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
σ : Semiformula ℒₒᵣ Empty 0
hσ : σ ∈ 𝐏𝐀⁻
⊢ (standardModelExp ℕ).toStruc ⊧ (Semiformula.lMap Language.oringEmb) σ
Tactic:
simpa [models_iff] using models_peanoMinus.realize hσ
State after:
no goals

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
⊢ ∀ (f : Sentence ℒₒᵣ(exp)) (x : Semiformula ℒₒᵣ(exp) ℕ 1),
    Hierarchy 𝚺 0 x → f = ∀ᶠ* succInd x → (standardModelExp ℕ).toStruc ⊧ f
Tactic:
rintro σ p _ rfl
State after:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
a✝ : Hierarchy 𝚺 0 p
⊢ (standardModelExp ℕ).toStruc ⊧ ∀ᶠ* succInd p

State before:
L : Language
inst✝⁸ : L.ORing
T : Theory L
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : L.Exp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Exp M
inst✝¹ : Mul M
inst✝ : LT M
p : Semiformula ℒₒᵣ(exp) ℕ 1
a✝ : Hierarchy 𝚺 0 p
⊢ (standardModelExp ℕ).toStruc ⊧ ∀ᶠ* succInd p
Tactic:
exact modelsSuccInd_exp p
State after:
no goals