internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x < f v, x ∈ f v → P v x
⊢ ∀ (x : Fin k → M), (∀ x_1 ∈ f x, P x x_1) ↔ ∀ x_1 < f x, x_1 ∈ f x → P x x_1
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x < f v, x ∈ f v → P v x
v : Fin k → M
⊢ (∀ x ∈ f v, P v x) ↔ ∀ x < f v, x ∈ f v → P v x
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x < f v, x ∈ f v → P v x
v : Fin k → M
⊢ (∀ x ∈ f v, P v x) ↔ ∀ x < f v, x ∈ f v → P v x
Tactic:
exact ⟨fun h x _ hxv ↦ h x hxv, fun h x hx ↦ h x (lt_of_mem hx) hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x
Tactic:
have : Definable ℒₒᵣ (Γ, m + 1) (fun v ↦ ∃ x < f v, x ∈ f v ∧ P v x) :=
  .bex_lt hf (.and (by simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)) h)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x
Tactic:
exact this.of_iff <| by
  intro v; exact ⟨by rintro ⟨x, hx, hxv⟩; exact ⟨x, lt_of_mem hx, hx, hxv⟩, by rintro ⟨x, _, hx, hvx⟩; exact ⟨x, hx, hvx⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ, m + 1) fun w => w 0 ∈ f fun x => w x.succ
Tactic:
simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction ℒₒᵣ (𝚺, m + 1) fun w => w 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ (Γ, m + 1)-Relation Membership.mem
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ ∀ (x : Fin k → M), (∃ x_1 ∈ f x, P x x_1) ↔ ∃ x_1 < f x, x_1 ∈ f x ∧ P x x_1
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x ∈ f v, P v x) ↔ ∃ x < f v, x ∈ f v ∧ P v x
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x ∈ f v, P v x) ↔ ∃ x < f v, x ∈ f v ∧ P v x
Tactic:
exact ⟨by rintro ⟨x, hx, hxv⟩; exact ⟨x, lt_of_mem hx, hx, hxv⟩, by rintro ⟨x, _, hx, hvx⟩; exact ⟨x, hx, hvx⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x ∈ f v, P v x) → ∃ x < f v, x ∈ f v ∧ P v x
Tactic:
rintro ⟨x, hx, hxv⟩
Proof 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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
hx : x ∈ f v
hxv : P v x
⊢ ∃ x < f v, x ∈ f v ∧ P v x
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof 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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
hx : x ∈ f v
hxv : P v x
⊢ ∃ x < f v, x ∈ f v ∧ P v x
Tactic:
exact ⟨x, lt_of_mem hx, hx, hxv⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
⊢ (∃ x < f v, x ∈ f v ∧ P v x) → ∃ x ∈ f v, P v x
Tactic:
rintro ⟨x, _, hx, hvx⟩
Proof state after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
left✝ : x < f v
hx : x ∈ f v
hvx : P v x
⊢ ∃ x ∈ f v, P v x
Theorem: LO.FirstOrder.Arith.Model.Definable.bex_mem
Proof state before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
v : Fin k → M
x : M
left✝ : x < f v
hx : x ∈ f v
hvx : P v x
⊢ ∃ x ∈ f v, P v x
Tactic:
exact ⟨x, hx, hvx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.operator_mem_def
Proof state before:
ξ : Type u_1
n : ?m.44108
⊢ op(∈).sentence = HSemiformula.val bitDef
Tactic:
simp [Semiformula.Operator.Mem.mem, Semiformula.Operator.operator]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bit
Proof state before:
ξ : Type u_1
n : ℕ
μ : Type u_2
Γ : Polarity
s : ℕ
t u : Semiterm ℒₒᵣ μ n
⊢ Hierarchy Γ s (“!!t ∈ !!u”)
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂, operator_mem_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hieralchy.ballIn
Proof state before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m (Arith.ballIn t p) ↔ Hierarchy Γ m p
Tactic:
simp only [Arith.ballIn, Rew.bshift_positive, Hierarchy.ball_iff, Hierarchy.imp_iff, and_iff_right_iff_imp]
Proof state after:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.ballLT t
        (“(#0 ∈ !!(Rew.bShift t) → !((Rew.substs (#0 :> fun x => #(BinderNotation.finSuccItr x 1))).hom p))”)) ↔
    Hierarchy Γ m p
Theorem: LO.FirstOrder.Arith.Hieralchy.ballIn
Proof state before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.ballLT t
        (“(#0 ∈ !!(Rew.bShift t) → !((Rew.substs (#0 :> fun x => #(BinderNotation.finSuccItr x 1))).hom p))”)) ↔
    Hierarchy Γ m p
Tactic:
simp [Semiformula.Operator.operator, operator_mem_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hieralchy.bexIn
Proof state before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m (Arith.bexIn t p) ↔ Hierarchy Γ m p
Tactic:
simp only [Arith.bexIn, Rew.bshift_positive, Hierarchy.bex_iff, Hierarchy.and_iff, and_iff_right_iff_imp]
Proof state after:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.bexLT t
        (“(#0 ∈ !!(Rew.bShift t) ∧ !((Rew.substs (#0 :> fun x => #(BinderNotation.finSuccItr x 1))).hom p))”)) ↔
    Hierarchy Γ m p
Theorem: LO.FirstOrder.Arith.Hieralchy.bexIn
Proof state before:
ξ : Type u_1
n : ℕ
Γ : Polarity
m : ℕ
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
⊢ Hierarchy Γ m
      (Semiformula.bexLT t
        (“(#0 ∈ !!(Rew.bShift t) ∧ !((Rew.substs (#0 :> fun x => #(BinderNotation.finSuccItr x 1))).hom p))”)) ↔
    Hierarchy Γ m p
Tactic:
simp [Semiformula.Operator.operator, operator_mem_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.memRel
Proof state before:
ξ : Type u_1
n : ℕ
μ : Type u_2
Γ : Polarity
s : ℕ
t₁ t₂ u : Semiterm ℒₒᵣ μ n
⊢ Hierarchy Γ s (memRelOpr.operator ![u, t₁, t₂])
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂, operator_mem_def, memRelOpr]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.eval_ballIn
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.eval_ballIn
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.eval_ballIn
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.eval_ballIn
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.eval_ballIn
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.eval_ballIn
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.eval_bexIn
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.eval_bexIn
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.eval_bexIn
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.eval_bexIn
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.eval_bexIn
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Arith.eval_bexIn
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Relation₃ fun r x y => ⟪x, y⟫ ∈ r via memRel
Tactic:
intro v
Proof state after:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (fun v => (fun r x y => ⟪x, y⟫ ∈ r) (v 0) (v 1) (v 2)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val memRel)
Theorem: LO.FirstOrder.Arith.Model.memRel_defined
Proof state before:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ (fun v => (fun r x y => ⟪x, y⟫ ∈ r) (v 0) (v 1) (v 2)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val memRel)
Tactic:
simp [memRel, pair_defined.df.iff, lt_succ_iff_le]
Proof state after:
ξ : Type u_1
n : ?m.110780
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 3 → M
⊢ ⟪v 1, v 2⟫ ∈ v 0 ↔ ∃ x ≤ (v 1 + v 2 + 1) ^ 2, x = ⟪v 1, v 2⟫ ∧ x ∈ v 0