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

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
x✝ : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ x✝) ⊤ → (Semiformula.Evalbm M fun x => ↑(x✝ x)) ⊤
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
x✝ : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ x✝) ⊥ → (Semiformula.Evalbm M fun x => ↑(x✝ x)) ⊥
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.rel op(=) v) → (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.rel op(=) v)
Tactic:
simp[Semiformula.eval_rel, Matrix.comp_vecCons', val_numeral]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.nrel op(=) v) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.nrel op(=) v)
Tactic:
simp[Semiformula.eval_nrel, Matrix.comp_vecCons', val_numeral]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.rel op(<) v) → (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.rel op(<) v)
Tactic:
simp[Semiformula.eval_rel, Matrix.comp_vecCons', val_numeral]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
v : Fin 2 → Semiterm ℒₒᵣ Empty n✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (Semiformula.nrel op(<) v) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (Semiformula.nrel op(<) v)
Tactic:
simp[Semiformula.eval_nrel, Matrix.comp_vecCons', val_numeral]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (p✝ ⋏ q✝) → (Semiformula.Evalbm M fun x => ↑(e x)) (p✝ ⋏ q✝)
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ →
    (Semiformula.Evalbm ℕ e) q✝ → (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ →
    (Semiformula.Evalbm ℕ e) q✝ → (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
intro ep eq
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
ep : (Semiformula.Evalbm ℕ e) p✝
eq : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
ep : (Semiformula.Evalbm ℕ e) p✝
eq : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∧ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
exact ⟨pval_of_pval_nat_of_sigma_one hp ep, pval_of_pval_nat_of_sigma_one hq eq⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (p✝ ⋎ q✝) → (Semiformula.Evalbm M fun x => ↑(e x)) (p✝ ⋎ q✝)
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ ∨ (Semiformula.Evalbm ℕ e) q✝ →
    (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) p✝ ∨ (Semiformula.Evalbm ℕ e) q✝ →
    (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
rintro (h | h)
State after:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

State before:
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
left
State after:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝

State before:
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) p✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝
Tactic:
exact pval_of_pval_nat_of_sigma_one hp h
State after:
no goals

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) p✝ ∨ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
right
State after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) q✝

State before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ : ℕ
p✝ q✝ : Semiformula ℒₒᵣ Empty a✝
hp : Hierarchy 𝚺 1 p✝
hq : Hierarchy 𝚺 1 q✝
e : Fin a✝ → ℕ
h : (Semiformula.Evalbm ℕ e) q✝
⊢ (Semiformula.Evalbm M fun x => ↑(e x)) q✝
Tactic:
exact pval_of_pval_nat_of_sigma_one hq h
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
t✝ : Semiterm ℒₒᵣ Empty (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (“(∀[#0 < !!t✝] !p✝)”) → (Semiformula.Evalbm M fun x => ↑(e x)) (“(∀[#0 < !!t✝] !p✝)”)
Tactic:
rcases Rew.positive_iff.mp pt with ⟨t, rfl⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (Semiformula.Evalbm ℕ e) (“(∀[#0 < !!(Rew.bShift t)] !p✝)”) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (“(∀[#0 < !!(Rew.bShift t)] !p✝)”)

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (Semiformula.Evalbm ℕ e) (“(∀[#0 < !!(Rew.bShift t)] !p✝)”) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (“(∀[#0 < !!(Rew.bShift t)] !p✝)”)
Tactic:
simp[val_numeral]
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝) →
    ∀ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
      (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝) →
    ∀ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
      (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
intro h x hx
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : M
hx : x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : M
hx : x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
rcases eq_nat_of_lt_nat hx with ⟨x, rfl⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : ℕ
hx : ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : ℕ
hx : ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp (h x (by simpa using hx))
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
h : ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t, (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
x : ℕ
hx : ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
⊢ x < Semiterm.val (standardModel ℕ) e Empty.elim t
Tactic:
simpa using hx
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
t✝ : Semiterm ℒₒᵣ Empty (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (“(∃[#0 < !!t✝] !p✝)”) → (Semiformula.Evalbm M fun x => ↑(e x)) (“(∃[#0 < !!t✝] !p✝)”)
Tactic:
rcases Rew.positive_iff.mp pt with ⟨t, rfl⟩
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (Semiformula.Evalbm ℕ e) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”)

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ (Semiformula.Evalbm ℕ e) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”) →
    (Semiformula.Evalbm M fun x => ↑(e x)) (“(∃[#0 < !!(Rew.bShift t)] !p✝)”)
Tactic:
simp[val_numeral]
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t,
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
        (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
⊢ ∀ x < Semiterm.val (standardModel ℕ) e Empty.elim t,
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
        (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
intro x hx h
State after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
    (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
    (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
exact ⟨x, by simpa using hx, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp h⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ↑x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t)
Tactic:
simpa using hx
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp h
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (∃' p) → (Semiformula.Evalbm M fun x => ↑(e x)) (∃' p)
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
intro x h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
have : Hierarchy 𝚺 1 p := hp.accum _
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
this : Hierarchy 𝚺 1 p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
this : Hierarchy 𝚺 1 p
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
exact ⟨x, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one this h⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚷 0 p
e : Fin n✝ → ℕ
x : ℕ
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p
this : Hierarchy 𝚺 1 p
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one this h
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
⊢ (Semiformula.Evalbm ℕ e) (∃' p✝) → (Semiformula.Evalbm M fun x => ↑(e x)) (∃' p✝)
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
⊢ ∀ (x : ℕ),
    (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝ →
      ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
intro x hx
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
x : ℕ
hx : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
x : ℕ
hx : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x, (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
exact ⟨x, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp hx⟩
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 (0 + 1) p✝
e : Fin n✝ → ℕ
x : ℕ
hx : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ (Semiformula.Eval (standardModel M) (↑x :> fun x => ↑(e x)) Empty.elim) p✝
Tactic:
simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp hx
State after:
no goals