Theorem: LO.FirstOrder.Arith.eval_bexIn (Arithmetization/ISigmaOne/Bit.lean)

State before:
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (Semiformula.Evalm M e ε) (bexIn t p) ↔ ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
simp [bexIn]
State after:
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p) ↔
    ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p

State before:
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p) ↔
    ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
constructor
State after:
case mp
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p) →
    ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p

case mpr
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p) →
    ∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p

State before:
case mp
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p) →
    ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
rintro ⟨x, _, hx, h⟩
State after:
case mp.intro.intro.intro
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
x : M
left✝ : x < Semiterm.val (standardModel M) e ε t
hx : x ∈ Semiterm.val (standardModel M) e ε t
h : (Semiformula.Eval (standardModel M) (x :> e) ε) p
⊢ ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p

State before:
case mp.intro.intro.intro
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
x : M
left✝ : x < Semiterm.val (standardModel M) e ε t
hx : x ∈ Semiterm.val (standardModel M) e ε t
h : (Semiformula.Eval (standardModel M) (x :> e) ε) p
⊢ ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
exact ⟨x, hx, h⟩
State after:
no goals

State before:
case mpr
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p) →
    ∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p
Tactic:
rintro ⟨x, hx, h⟩
State after:
case mpr.intro.intro
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
x : M
hx : x ∈ Semiterm.valm M e ε t
h : (Semiformula.Evalm M (x :> e) ε) p
⊢ ∃ x < Semiterm.val (standardModel M) e ε t,
    x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p

State before:
case mpr.intro.intro
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
x : M
hx : x ∈ Semiterm.valm M e ε t
h : (Semiformula.Evalm M (x :> e) ε) p
⊢ ∃ x < Semiterm.val (standardModel M) e ε t,
    x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p
Tactic:
exact ⟨x, lt_of_mem hx, hx, h⟩
State after:
no goals