Theorem: LO.FirstOrder.Arith.eval_ballIn (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 ε) (ballIn t p) ↔ ∀ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
simp [ballIn]
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:
intro h x hx
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
h :
  ∀ x < Semiterm.val (standardModel M) e ε t,
    x ∈ Semiterm.val (standardModel M) e ε t → (Semiformula.Eval (standardModel M) (x :> e) ε) p
x : M
hx : x ∈ Semiterm.valm M e ε t
⊢ (Semiformula.Evalm 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
h :
  ∀ x < Semiterm.val (standardModel M) e ε t,
    x ∈ Semiterm.val (standardModel M) e ε t → (Semiformula.Eval (standardModel M) (x :> e) ε) p
x : M
hx : x ∈ Semiterm.valm M e ε t
⊢ (Semiformula.Evalm M (x :> e) ε) p
Tactic:
exact h x (lt_of_mem hx) hx
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:
intro h x _ hx
State after:
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
h : ∀ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
x : M
a✝ : x < Semiterm.val (standardModel M) e ε t
hx : x ∈ Semiterm.val (standardModel M) e ε t
⊢ (Semiformula.Eval (standardModel M) (x :> e) ε) p

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
h : ∀ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
x : M
a✝ : x < Semiterm.val (standardModel M) e ε t
hx : x ∈ Semiterm.val (standardModel M) e ε t
⊢ (Semiformula.Eval (standardModel M) (x :> e) ε) p
Tactic:
exact h x hx
State after:
no goals