internlm/Lean-Github huggingface dataset:
Theorem: Arith.Model.Defined.to_definable
Proof state before:
case mkDelta
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
snd✝ : ℕ
v : Fin k → M
a✝¹ : HSemiformula L Empty k (𝚺, snd✝)
a✝ : HSemiformula L Empty k (𝚷, snd✝)
hP : Defined P (a✝¹.mkDelta a✝)
⊢ (Semiformula.Evalm M v id) (HSemiformula.rew Rew.emb (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalm M v id) (HSemiformula.rew Rew.emb (a✝¹.mkDelta a✝)).pi.val
Tactic:
simpa [HSemiformula.rew] using hP.proper.rew Rew.emb v
Proof state after:
no goals
Theorem: Arith.Model.Defined.to_definable
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
snd✝ : ℕ
p : HSemisentence L k (𝚫, snd✝)
hP : Defined P p
⊢ FirstOrder.DefinedWithParam P (HSemiformula.rew Rew.emb p).val
Tactic:
intro
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
snd✝ : ℕ
p : HSemisentence L k (𝚫, snd✝)
hP : Defined P p
v✝ : Fin k → M
⊢ P v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.rew Rew.emb p).val
Theorem: Arith.Model.Defined.to_definable
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
snd✝ : ℕ
p : HSemisentence L k (𝚫, snd✝)
hP : Defined P p
v✝ : Fin k → M
⊢ P v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.rew Rew.emb p).val
Tactic:
simp [hP.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.DefinedFunction.of_eq
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f g : (Fin k → M) → M
h : ∀ (x : Fin k → M), f x = g x
p : HSemisentence L (k + 1) Γ
H : DefinedFunction L Γ f p
⊢ ∀ (x : Fin k.succ → M), (x 0 = g fun x_1 => x x_1.succ) ↔ x 0 = f fun x_1 => x x_1.succ
Tactic:
intro
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f g : (Fin k → M) → M
h : ∀ (x : Fin k → M), f x = g x
p : HSemisentence L (k + 1) Γ
H : DefinedFunction L Γ f p
x✝ : Fin k.succ → M
⊢ (x✝ 0 = g fun x => x✝ x.succ) ↔ x✝ 0 = f fun x => x✝ x.succ
Theorem: Arith.Model.DefinedFunction.of_eq
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f g : (Fin k → M) → M
h : ∀ (x : Fin k → M), f x = g x
p : HSemisentence L (k + 1) Γ
H : DefinedFunction L Γ f p
x✝ : Fin k.succ → M
⊢ (x✝ 0 = g fun x => x✝ x.succ) ↔ x✝ 0 = f fun x => x✝ x.succ
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Arith.Model.DefinedFunction.graph_delta
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
f : (Fin k → M) → M
p : HSemisentence L (k + 1) (𝚺, m)
h : DefinedFunction L (𝚺, m) f p
⊢ HSemiformula.ProperOn M (HSemiformula.graphDelta p)
Tactic:
cases' m with m <;> simp [HSemiformula.graphDelta]
Proof state after:
case succ
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : (Fin k → M) → M
m : ℕ
p : HSemisentence L (k + 1) (𝚺, m + 1)
h : DefinedFunction L (𝚺, m + 1) f p
⊢ HSemiformula.ProperOn M
    (HSemiformula.mkDelta p
      (HSemiformula.mkPi (“∀' (!((Rew.substs (#0 :> fun x => #x.succ.succ)).hom (HSemiformula.val p)) → #0 = #1)”) ⋯))
Theorem: Arith.Model.DefinedFunction.graph_delta
Proof state before:
case succ
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : (Fin k → M) → M
m : ℕ
p : HSemisentence L (k + 1) (𝚺, m + 1)
h : DefinedFunction L (𝚺, m + 1) f p
⊢ HSemiformula.ProperOn M
    (HSemiformula.mkDelta p
      (HSemiformula.mkPi (“∀' (!((Rew.substs (#0 :> fun x => #x.succ.succ)).hom (HSemiformula.val p)) → #0 = #1)”) ⋯))
Tactic:
intro e
Proof state after:
case succ
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : (Fin k → M) → M
m : ℕ
p : HSemisentence L (k + 1) (𝚺, m + 1)
h : DefinedFunction L (𝚺, m + 1) f p
e : Fin (k + 1) → M
⊢ (Semiformula.Evalbm M e)
      (HSemiformula.mkDelta p
            (HSemiformula.mkPi (“∀' (!((Rew.substs (#0 :> fun x => #x.succ.succ)).hom (HSemiformula.val p)) → #0 = #1)”)
              ⋯)).sigma.val ↔
    (Semiformula.Evalbm M e)
      (HSemiformula.mkDelta p
            (HSemiformula.mkPi (“∀' (!((Rew.substs (#0 :> fun x => #x.succ.succ)).hom (HSemiformula.val p)) → #0 = #1)”)
              ⋯)).pi.val
Theorem: Arith.Model.DefinedFunction.graph_delta
Proof state before:
case succ
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : (Fin k → M) → M
m : ℕ
p : HSemisentence L (k + 1) (𝚺, m + 1)
h : DefinedFunction L (𝚺, m + 1) f p
e : Fin (k + 1) → M
⊢ (Semiformula.Evalbm M e)
      (HSemiformula.mkDelta p
            (HSemiformula.mkPi (“∀' (!((Rew.substs (#0 :> fun x => #x.succ.succ)).hom (HSemiformula.val p)) → #0 = #1)”)
              ⋯)).sigma.val ↔
    (Semiformula.Evalbm M e)
      (HSemiformula.mkDelta p
            (HSemiformula.mkPi (“∀' (!((Rew.substs (#0 :> fun x => #x.succ.succ)).hom (HSemiformula.val p)) → #0 = #1)”)
              ⋯)).pi.val
Tactic:
simp [Empty.eq_elim, h.df.iff]
Proof state after:
case succ
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : (Fin k → M) → M
m : ℕ
p : HSemisentence L (k + 1) (𝚺, m + 1)
h : DefinedFunction L (𝚺, m + 1) f p
e : Fin (k + 1) → M
⊢ (e 0 = f fun x => e x.succ) ↔ (f fun x => e x.succ) = e 0
Theorem: Arith.Model.DefinedFunction.graph_delta
Proof state before:
case succ
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
f : (Fin k → M) → M
m : ℕ
p : HSemisentence L (k + 1) (𝚺, m + 1)
h : DefinedFunction L (𝚺, m + 1) f p
e : Fin (k + 1) → M
⊢ (e 0 = f fun x => e x.succ) ↔ (f fun x => e x.succ) = e 0
Tactic:
rw [eq_comm]
Proof state after:
no goals
Theorem: Arith.Model.DefinedFunction.graph_delta
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
f : (Fin k → M) → M
p : HSemisentence L (k + 1) (𝚺, m)
h : DefinedFunction L (𝚺, m) f p
⊢ FirstOrder.Defined (fun v => v 0 = f fun x => v x.succ) (HSemiformula.graphDelta p).val
Tactic:
intro v
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
f : (Fin k → M) → M
p : HSemisentence L (k + 1) (𝚺, m)
h : DefinedFunction L (𝚺, m) f p
v : Fin k.succ → M
⊢ (fun v => v 0 = f fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.graphDelta p).val
Theorem: Arith.Model.DefinedFunction.graph_delta
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
m : ℕ
f : (Fin k → M) → M
p : HSemisentence L (k + 1) (𝚺, m)
h : DefinedFunction L (𝚺, m) f p
v : Fin k.succ → M
⊢ (fun v => v 0 = f fun x => v x.succ) v ↔ (Semiformula.Evalbm M v) (HSemiformula.graphDelta p).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
⊢ DefinedWithParam R (p.ofZero (𝚺, m))
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofZero (𝚺, m)).val
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofZero (𝚺, m)).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
⊢ DefinedWithParam R (p.ofZero (𝚷, m))
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofZero (𝚷, m)).val
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofZero (𝚷, m)).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
⊢ HSemiformula.ProperWithParamOn M (p.ofZero (𝚫, m))
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
⊢ FirstOrder.DefinedWithParam R (p.ofZero (𝚫, m)).val
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofZero (𝚫, m)).val
Theorem: Arith.Model.DefinedWithParam.of_zero
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q : (Fin k → M) → Prop
Γ' : SigmaPiDelta
R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemiformula L M k (Γ', 0)
h : DefinedWithParam R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofZero (𝚫, m)).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
⊢ DefinedWithParam R (p.ofDeltaOne 𝚺 m)
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofDeltaOne 𝚺 m).val
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofDeltaOne 𝚺 m).val
Tactic:
simp [HSemiformula.ofDeltaOne, h.df.iff, HSemiformula.val_sigma]
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
⊢ DefinedWithParam R (p.ofDeltaOne 𝚷 m)
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofDeltaOne 𝚷 m).val
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofDeltaOne 𝚷 m).val
Tactic:
simp [HSemiformula.ofDeltaOne, h.df.iff, h.proper.iff']
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
⊢ HSemiformula.ProperWithParamOn M (p.ofDeltaOne 𝚫 m)
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
e✝ : Fin k → M
⊢ (Semiformula.Evalm M e✝ id) (p.ofDeltaOne 𝚫 m).sigma.val ↔ (Semiformula.Evalm M e✝ id) (p.ofDeltaOne 𝚫 m).pi.val
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
e✝ : Fin k → M
⊢ (Semiformula.Evalm M e✝ id) (p.ofDeltaOne 𝚫 m).sigma.val ↔ (Semiformula.Evalm M e✝ id) (p.ofDeltaOne 𝚫 m).pi.val
Tactic:
simp [HSemiformula.ofDeltaOne, h.df.iff, HSemiformula.val_sigma, h.proper.iff']
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
⊢ FirstOrder.DefinedWithParam R (p.ofDeltaOne 𝚫 m).val
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofDeltaOne 𝚫 m).val
Theorem: Arith.Model.DefinedWithParam.of_deltaOne
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L M k 𝚫₁
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (p.ofDeltaOne 𝚫 m).val
Tactic:
simp [HSemiformula.ofDeltaOne, h.df.iff, HSemiformula.val_sigma]
Proof state after:
no goals
Theorem: Arith.Model.DefinedWithParam.emb
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : HierarchySymbol
m : ℕ
p : HSemiformula ℒₒᵣ M k (𝚺, m)
h : DefinedWithParam R p
⊢ DefinedWithParam R (HSemiformula.emb L p)
Tactic:
intro _
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : HierarchySymbol
m : ℕ
p : HSemiformula ℒₒᵣ M k (𝚺, m)
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.emb L p).val
Theorem: Arith.Model.DefinedWithParam.emb
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P Q R : (Fin k → M) → Prop
Γ : HierarchySymbol
m : ℕ
p : HSemiformula ℒₒᵣ M k (𝚺, m)
h : DefinedWithParam R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalm M v✝ id) (HSemiformula.emb L p).val
Tactic:
simp [h.iff]
Proof state after:
no goals