internlm/Lean-Github huggingface dataset:
Theorem: Arith.HSemiformula.ProperWithParamOn.neg
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
p : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (~p).sigma.val ↔ (Semiformula.Evalm M e id) (~p).pi.val
Tactic:
simp [hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.eval_neg
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
p : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (~p).val ↔ ¬(Semiformula.Evalm M e id) p.val
Tactic:
simp [val, ←val_sigma, hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.ball
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
t : Semiterm L M k
p : HSemiformula L M (k + 1) (𝚫, m)
hp : ProperWithParamOn M p
⊢ ProperWithParamOn M (HSemiformula.ball t p)
Tactic:
intro e
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
t : Semiterm L M k
p : HSemiformula L M (k + 1) (𝚫, m)
hp : ProperWithParamOn M p
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.ball t p).sigma.val ↔
    (Semiformula.Evalm M e id) (HSemiformula.ball t p).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.ball
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
t : Semiterm L M k
p : HSemiformula L M (k + 1) (𝚫, m)
hp : ProperWithParamOn M p
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.ball t p).sigma.val ↔
    (Semiformula.Evalm M e id) (HSemiformula.ball t p).pi.val
Tactic:
simp [HSemiformula.ball, hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.bex
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
t : Semiterm L M k
p : HSemiformula L M (k + 1) (𝚫, m)
hp : ProperWithParamOn M p
⊢ ProperWithParamOn M (HSemiformula.bex t p)
Tactic:
intro e
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
t : Semiterm L M k
p : HSemiformula L M (k + 1) (𝚫, m)
hp : ProperWithParamOn M p
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.bex t p).sigma.val ↔ (Semiformula.Evalm M e id) (HSemiformula.bex t p).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.bex
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
t : Semiterm L M k
p : HSemiformula L M (k + 1) (𝚫, m)
hp : ProperWithParamOn M p
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.bex t p).sigma.val ↔ (Semiformula.Evalm M e id) (HSemiformula.bex t p).pi.val
Tactic:
simp [HSemiformula.bex, hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.graphDelta_val
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k m : ℕ
p : HSemiformula L ξ (k + 1) (𝚺, m)
⊢ p.graphDelta.val = p.val
Tactic:
cases m <;> simp [graphDelta]
Proof state after:
no goals
Theorem: Arith.Definability.HSemiformula.hierarchy_zero
Proof state before:
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ✝ : SigmaPiDelta
m✝ : ℕ
Γ : SigmaPiDelta
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (Γ, 0)
⊢ Hierarchy Γ' m p.val
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.sigma, 0)
⊢ Hierarchy Γ' m p.val

case pi
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.pi, 0)
⊢ Hierarchy Γ' m p.val

case delta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.delta, 0)
⊢ Hierarchy Γ' m p.val
Theorem: Arith.Definability.HSemiformula.hierarchy_zero
Proof state before:
case sigma
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.sigma, 0)
⊢ Hierarchy Γ' m p.val
Tactic:
exact Hierarchy.of_zero p.sigma_prop
Proof state after:
no goals
Theorem: Arith.Definability.HSemiformula.hierarchy_zero
Proof state before:
case pi
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.pi, 0)
⊢ Hierarchy Γ' m p.val
Tactic:
exact Hierarchy.of_zero p.pi_prop
Proof state after:
no goals
Theorem: Arith.Definability.HSemiformula.hierarchy_zero
Proof state before:
case delta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.delta, 0)
⊢ Hierarchy Γ' m p.val
Tactic:
cases p
Proof state after:
case delta.mkDelta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, 0)
a✝ : HSemiformula L ξ n (𝚷, 0)
⊢ Hierarchy Γ' m (a✝¹.mkDelta a✝).val
Theorem: Arith.Definability.HSemiformula.hierarchy_zero
Proof state before:
case delta.mkDelta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, 0)
a✝ : HSemiformula L ξ n (𝚷, 0)
⊢ Hierarchy Γ' m (a✝¹.mkDelta a✝).val
Tactic:
simp
Proof state after:
case delta.mkDelta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, 0)
a✝ : HSemiformula L ξ n (𝚷, 0)
⊢ Hierarchy Γ' m a✝¹.val
Theorem: Arith.Definability.HSemiformula.hierarchy_zero
Proof state before:
case delta.mkDelta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, 0)
a✝ : HSemiformula L ξ n (𝚷, 0)
⊢ Hierarchy Γ' m a✝¹.val
Tactic:
exact Hierarchy.of_zero (HSemiformula.sigma_prop _)
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
⊢ Defined R (HSemiformula.ofZero p (𝚺, 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
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.ofZero p (𝚺, m)).val
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.ofZero p (𝚺, m)).val
Tactic:
simp [h.iff]
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
⊢ Defined R (HSemiformula.ofZero p (𝚷, 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
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.ofZero p (𝚷, m)).val
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.ofZero p (𝚷, m)).val
Tactic:
simp [h.iff]
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
⊢ HSemiformula.ProperOn M (HSemiformula.ofZero p (𝚫, m))
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
⊢ FirstOrder.Defined R (HSemiformula.ofZero p (𝚫, 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
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.ofZero p (𝚫, m)).val
Theorem: Arith.Model.Defined.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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
p : HSemisentence L k (𝚺, 0)
h : Defined R p
m : ℕ
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.ofZero p (𝚫, m)).val
Tactic:
simp [h.iff]
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 : (𝚺, m)-Semisentence k
h : Defined R p
⊢ Defined 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 : (𝚺, m)-Semisentence k
h : Defined R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.emb L p).val
Theorem: Arith.Model.Defined.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 : (𝚺, m)-Semisentence k
h : Defined R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.emb L p).val
Tactic:
simp [h.iff]
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 : (𝚷, m)-Semisentence k
h : Defined R p
⊢ Defined 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 : (𝚷, m)-Semisentence k
h : Defined R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.emb L p).val
Theorem: Arith.Model.Defined.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 : (𝚷, m)-Semisentence k
h : Defined R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.emb L p).val
Tactic:
simp [h.iff]
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 : (𝚫, m)-Semisentence k
h : Defined R p
⊢ HSemiformula.ProperOn M (HSemiformula.emb L p)
Tactic:
simpa using h.proper
Proof state after:
no goals
Theorem: Arith.Model.Defined.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 : (𝚫, m)-Semisentence k
h : Defined R p
⊢ FirstOrder.Defined R (HSemiformula.emb L 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 R : (Fin k → M) → Prop
Γ : HierarchySymbol
m : ℕ
p : (𝚫, m)-Semisentence k
h : Defined R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.emb L p).val
Theorem: Arith.Model.Defined.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 : (𝚫, m)-Semisentence k
h : Defined R p
v✝ : Fin k → M
⊢ R v✝ ↔ (Semiformula.Evalbm M v✝) (HSemiformula.emb L p).val
Tactic:
simp [h.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.Defined.of_iff
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✝ P Q : (Fin k → M) → Prop
h : ∀ (x : Fin k → M), P x ↔ Q x
p : HSemisentence L k Γ
H : Defined Q p
⊢ Defined P p
Tactic:
rwa [show P = Q from by funext v; simp [h]]
Proof state after:
no goals
Theorem: Arith.Model.Defined.of_iff
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✝ P Q : (Fin k → M) → Prop
h : ∀ (x : Fin k → M), P x ↔ Q x
p : HSemisentence L k Γ
H : Defined Q p
⊢ P = Q
Tactic:
funext v
Proof state after:
case h
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✝ P Q : (Fin k → M) → Prop
h : ∀ (x : Fin k → M), P x ↔ Q x
p : HSemisentence L k Γ
H : Defined Q p
v : Fin k → M
⊢ P v = Q v
Theorem: Arith.Model.Defined.of_iff
Proof state before:
case h
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✝ P Q : (Fin k → M) → Prop
h : ∀ (x : Fin k → M), P x ↔ Q x
p : HSemisentence L k Γ
H : Defined Q p
v : Fin k → M
⊢ P v = Q v
Tactic:
simp [h]
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
p : HSemisentence L k Γ
hP : Defined P p
⊢ DefinedWithParam P (HSemiformula.rew Rew.emb p)
Tactic:
match Γ with
| (𝚺, _) => intro; simp [hP.iff]
| (𝚷, _) => intro; simp [hP.iff]
| (𝚫, _) => exact ⟨
  fun v ↦ by rcases p; simpa [HSemiformula.rew] using hP.proper.rew Rew.emb v,
  by intro; simp [hP.df.iff]⟩
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
⊢ DefinedWithParam P (HSemiformula.rew Rew.emb 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 : (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.iff]
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
⊢ DefinedWithParam P (HSemiformula.rew Rew.emb 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 : (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.iff]
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
⊢ DefinedWithParam P (HSemiformula.rew Rew.emb p)
Tactic:
exact ⟨
fun v ↦ by rcases p; simpa [HSemiformula.rew] using hP.proper.rew Rew.emb v,
by intro; simp [hP.df.iff]⟩
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
v : Fin k → M
⊢ (Semiformula.Evalm M v id) (HSemiformula.rew Rew.emb p).sigma.val ↔
    (Semiformula.Evalm M v id) (HSemiformula.rew Rew.emb p).pi.val
Tactic:
rcases p
Proof state after:
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