internlm/Lean-Github huggingface dataset:
Theorem: Arith.HSemiformula.val_verum
Proof state before:
case mk
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
Γ : SigmaPiDelta
m : ℕ
⊢ ⊤.val = ⊤
Tactic:
rcases Γ <;> simp [val]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_verum
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
m : ℕ
⊢ ⊤.sigma = ⊤
Tactic:
simp [Top.top, verum]
Proof state after:
no goals
Theorem: Arith.HSemiformula.pi_verum
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
m : ℕ
⊢ ⊤.pi = ⊤
Tactic:
simp [Top.top, verum]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_falsum
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
Γ : HierarchySymbol
⊢ ⊥.val = ⊥
Tactic:
rcases Γ with ⟨Γ, m⟩
Proof state after:
case mk
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
Γ : SigmaPiDelta
m : ℕ
⊢ ⊥.val = ⊥
Theorem: Arith.HSemiformula.val_falsum
Proof state before:
case mk
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
Γ : SigmaPiDelta
m : ℕ
⊢ ⊥.val = ⊥
Tactic:
rcases Γ <;> simp [val]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_falsum
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
m : ℕ
⊢ ⊥.sigma = ⊥
Tactic:
simp [Bot.bot, falsum]
Proof state after:
no goals
Theorem: Arith.HSemiformula.pi_falsum
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
m : ℕ
⊢ ⊥.pi = ⊥
Tactic:
simp [Bot.bot, falsum]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_and
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
Γ : HierarchySymbol
p q : HSemiformula L ξ n Γ
⊢ (p ⋏ q).val = p.val ⋏ q.val
Tactic:
rcases Γ with ⟨Γ, m⟩
Proof state after:
case mk
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
Γ : SigmaPiDelta
m : ℕ
p q : HSemiformula L ξ n (Γ, m)
⊢ (p ⋏ q).val = p.val ⋏ q.val
Theorem: Arith.HSemiformula.val_and
Proof state before:
case mk
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
Γ : SigmaPiDelta
m : ℕ
p q : HSemiformula L ξ n (Γ, m)
⊢ (p ⋏ q).val = p.val ⋏ q.val
Tactic:
rcases Γ <;> simp [val, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_and
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
m : ℕ
p q : HSemiformula L ξ n (𝚫, m)
⊢ (p ⋏ q).sigma = p.sigma ⋏ q.sigma
Tactic:
simp [Wedge.wedge, and]
Proof state after:
no goals
Theorem: Arith.HSemiformula.pi_and
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
m : ℕ
p q : HSemiformula L ξ n (𝚫, m)
⊢ (p ⋏ q).pi = p.pi ⋏ q.pi
Tactic:
simp [Wedge.wedge, and]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_or
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
Γ : HierarchySymbol
p q : HSemiformula L ξ n Γ
⊢ (p ⋎ q).val = p.val ⋎ q.val
Tactic:
rcases Γ with ⟨Γ, m⟩
Proof state after:
case mk
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
Γ : SigmaPiDelta
m : ℕ
p q : HSemiformula L ξ n (Γ, m)
⊢ (p ⋎ q).val = p.val ⋎ q.val
Theorem: Arith.HSemiformula.val_or
Proof state before:
case mk
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
Γ : SigmaPiDelta
m : ℕ
p q : HSemiformula L ξ n (Γ, m)
⊢ (p ⋎ q).val = p.val ⋎ q.val
Tactic:
rcases Γ <;> simp [val, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_or
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
m : ℕ
p q : HSemiformula L ξ n (𝚫, m)
⊢ (p ⋎ q).sigma = p.sigma ⋎ q.sigma
Tactic:
simp [Vee.vee, or]
Proof state after:
no goals
Theorem: Arith.HSemiformula.pi_or
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
m : ℕ
p q : HSemiformula L ξ n (𝚫, m)
⊢ (p ⋎ q).pi = p.pi ⋎ q.pi
Tactic:
simp [Vee.vee, or]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_negSigma
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
m : ℕ
p : HSemiformula L ξ n (𝚺, m)
⊢ p.negSigma.val = ~p.val
Tactic:
simp [val, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_negPi
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
m : ℕ
p : HSemiformula L ξ n (𝚷, m)
⊢ p.negPi.val = ~p.val
Tactic:
simp [val, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_negDelta
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
m : ℕ
p : HSemiformula L ξ n (𝚫, m)
⊢ (~p).val = ~p.pi.val
Tactic:
simp [Tilde.tilde, negDelta]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_negDelta
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
m : ℕ
p : HSemiformula L ξ n (𝚫, m)
⊢ (~p).sigma = p.pi.negPi
Tactic:
simp [Tilde.tilde, negDelta]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_negPi
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
m : ℕ
p : HSemiformula L ξ n (𝚫, m)
⊢ (~p).pi = p.sigma.negSigma
Tactic:
simp [Tilde.tilde, negDelta]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_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
Γ : HierarchySymbol
t : Semiterm L ξ n
p : HSemiformula L ξ (n + 1) Γ
⊢ (ball t p).val = (“(∀[#0 < !!(Rew.bShift t)] !p.val)”)
Tactic:
rcases Γ with ⟨Γ, m⟩
Proof state after:
case mk
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
t : Semiterm L ξ n
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L ξ (n + 1) (Γ, m)
⊢ (ball t p).val = (“(∀[#0 < !!(Rew.bShift t)] !p.val)”)
Theorem: Arith.HSemiformula.val_ball
Proof state before:
case mk
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
t : Semiterm L ξ n
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L ξ (n + 1) (Γ, m)
⊢ (ball t p).val = (“(∀[#0 < !!(Rew.bShift t)] !p.val)”)
Tactic:
rcases Γ <;> simp [val, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_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
Γ : HierarchySymbol
t : Semiterm L ξ n
p : HSemiformula L ξ (n + 1) Γ
⊢ (bex t p).val = (“(∃[#0 < !!(Rew.bShift t)] !p.val)”)
Tactic:
rcases Γ with ⟨Γ, m⟩
Proof state after:
case mk
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
t : Semiterm L ξ n
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L ξ (n + 1) (Γ, m)
⊢ (bex t p).val = (“(∃[#0 < !!(Rew.bShift t)] !p.val)”)
Theorem: Arith.HSemiformula.val_bex
Proof state before:
case mk
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
t : Semiterm L ξ n
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula L ξ (n + 1) (Γ, m)
⊢ (bex t p).val = (“(∃[#0 < !!(Rew.bShift t)] !p.val)”)
Tactic:
rcases Γ <;> simp [val, val_sigma]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.verum
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 : ℕ
⊢ ProperOn M ⊤
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma ⊤).val ↔ (Semiformula.Evalbm M e) (pi ⊤).val
Theorem: Arith.HSemiformula.ProperOn.verum
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma ⊤).val ↔ (Semiformula.Evalbm M e) (pi ⊤).val
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.falsum
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 : ℕ
⊢ ProperOn M ⊥
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma ⊥).val ↔ (Semiformula.Evalbm M e) (pi ⊥).val
Theorem: Arith.HSemiformula.ProperOn.falsum
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma ⊥).val ↔ (Semiformula.Evalbm M e) (pi ⊥).val
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.and
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 q : HSemisentence L k (𝚫, m)
hp : ProperOn M p
hq : ProperOn M q
⊢ ProperOn M (p ⋏ q)
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 : ℕ
p q : HSemisentence L k (𝚫, m)
hp : ProperOn M p
hq : ProperOn M q
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma (p ⋏ q)).val ↔ (Semiformula.Evalbm M e) (pi (p ⋏ q)).val
Theorem: Arith.HSemiformula.ProperOn.and
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 q : HSemisentence L k (𝚫, m)
hp : ProperOn M p
hq : ProperOn M q
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma (p ⋏ q)).val ↔ (Semiformula.Evalbm M e) (pi (p ⋏ q)).val
Tactic:
simp [hp.iff, hq.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.or
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 q : HSemisentence L k (𝚫, m)
hp : ProperOn M p
hq : ProperOn M q
⊢ ProperOn M (p ⋎ q)
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 : ℕ
p q : HSemisentence L k (𝚫, m)
hp : ProperOn M p
hq : ProperOn M q
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma (p ⋎ q)).val ↔ (Semiformula.Evalbm M e) (pi (p ⋎ q)).val
Theorem: Arith.HSemiformula.ProperOn.or
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 q : HSemisentence L k (𝚫, m)
hp : ProperOn M p
hq : ProperOn M q
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma (p ⋎ q)).val ↔ (Semiformula.Evalbm M e) (pi (p ⋎ q)).val
Tactic:
simp [hp.iff, hq.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.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 : HSemisentence L k (𝚫, m)
hp : ProperOn M p
⊢ ProperOn M (~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 : ℕ
p : HSemisentence L k (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma (~p)).val ↔ (Semiformula.Evalbm M e) (pi (~p)).val
Theorem: Arith.HSemiformula.ProperOn.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 : HSemisentence L k (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (sigma (~p)).val ↔ (Semiformula.Evalbm M e) (pi (~p)).val
Tactic:
simp [hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.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 : HSemisentence L k (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (val (~p)) ↔ ¬(Semiformula.Evalbm M e) (val p)
Tactic:
simp [val, ←val_sigma, hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.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 Empty k
p : HSemisentence L (k + 1) (𝚫, m)
hp : ProperOn M p
⊢ ProperOn 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 Empty k
p : HSemisentence L (k + 1) (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.ball t p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.ball t p).pi.val
Theorem: Arith.HSemiformula.ProperOn.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 Empty k
p : HSemisentence L (k + 1) (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.ball t p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.ball t p).pi.val
Tactic:
simp [HSemiformula.ball, hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.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 Empty k
p : HSemisentence L (k + 1) (𝚫, m)
hp : ProperOn M p
⊢ ProperOn 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 Empty k
p : HSemisentence L (k + 1) (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.bex t p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.bex t p).pi.val
Theorem: Arith.HSemiformula.ProperOn.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 Empty k
p : HSemisentence L (k + 1) (𝚫, m)
hp : ProperOn M p
e : Fin k → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.bex t p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.bex t p).pi.val
Tactic:
simp [HSemiformula.bex, hp.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.verum
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 : ℕ
⊢ ProperWithParamOn M ⊤
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalm M e id) ⊤.sigma.val ↔ (Semiformula.Evalm M e id) ⊤.pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.verum
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalm M e id) ⊤.sigma.val ↔ (Semiformula.Evalm M e id) ⊤.pi.val
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.falsum
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 : ℕ
⊢ ProperWithParamOn M ⊥
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalm M e id) ⊥.sigma.val ↔ (Semiformula.Evalm M e id) ⊥.pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.falsum
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 : ℕ
e : Fin k → M
⊢ (Semiformula.Evalm M e id) ⊥.sigma.val ↔ (Semiformula.Evalm M e id) ⊥.pi.val
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.and
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 q : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
hq : ProperWithParamOn M q
⊢ ProperWithParamOn M (p ⋏ q)
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 : ℕ
p q : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
hq : ProperWithParamOn M q
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (p ⋏ q).sigma.val ↔ (Semiformula.Evalm M e id) (p ⋏ q).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.and
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 q : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
hq : ProperWithParamOn M q
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (p ⋏ q).sigma.val ↔ (Semiformula.Evalm M e id) (p ⋏ q).pi.val
Tactic:
simp [hp.iff, hq.iff]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.or
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 q : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
hq : ProperWithParamOn M q
⊢ ProperWithParamOn M (p ⋎ q)
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 : ℕ
p q : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
hq : ProperWithParamOn M q
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (p ⋎ q).sigma.val ↔ (Semiformula.Evalm M e id) (p ⋎ q).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.or
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 q : HSemiformula L M k (𝚫, m)
hp : ProperWithParamOn M p
hq : ProperWithParamOn M q
e : Fin k → M
⊢ (Semiformula.Evalm M e id) (p ⋎ q).sigma.val ↔ (Semiformula.Evalm M e id) (p ⋎ q).pi.val
Tactic:
simp [hp.iff, hq.iff]
Proof state after:
no goals
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
⊢ ProperWithParamOn M (~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 : ℕ
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