Theorem: LO.FirstOrder.Arith.Standard.modelsSuccInd_exp (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
p : Semiformula ℒₒᵣ(exp) ℕ 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]
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
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModelExp ℕ) ![0] ε) p →
      (∀ (x : ℕ),
          (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] ε) 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
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModelExp ℕ) ![0] ε) p →
      (∀ (x : ℕ),
          (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] ε) p
Tactic:
intro e hzero hsucc x
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
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x] e) 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
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
Tactic:
induction' x with x ih
State after:
case zero
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
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![0] e) p

case succ
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
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
ih : (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p

State before:
case zero
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
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
Tactic:
exact hzero
State after:
no goals

State before:
case succ
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
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModelExp ℕ) ![0] e) p
hsucc :
  ∀ (x : ℕ), (Semiformula.Eval (standardModelExp ℕ) ![x] e) p → (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
x : ℕ
ih : (Semiformula.Eval (standardModelExp ℕ) ![x] e) p
⊢ (Semiformula.Eval (standardModelExp ℕ) ![x + 1] e) p
Tactic:
exact hsucc x ih
State after:
no goals