internlm/Lean-Github huggingface dataset:
Theorem: Arith.HSemiformula.ProperOn.rew
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
n₁ m n₂ : ℕ
p : HSemisentence L n₁ (𝚫, m)
h : ProperOn M p
ω : Rew L Empty n₁ Empty n₂
⊢ ProperOn M (HSemiformula.rew ω p)
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ ProperOn M (HSemiformula.rew ω (a✝¹.mkDelta a✝))
Theorem: Arith.HSemiformula.ProperOn.rew
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ ProperOn M (HSemiformula.rew ω (a✝¹.mkDelta a✝))
Tactic:
simp [ProperOn, HSemiformula.rew, Semiformula.eval_rew, Function.comp, h.iff, Empty.eq_elim]
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ ∀ (e : Fin n₂ → M),
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝¹.val ↔
      (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝.val
Theorem: Arith.HSemiformula.ProperOn.rew
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ ∀ (e : Fin n₂ → M),
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝¹.val ↔
      (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝.val
Tactic:
intro e
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝¹.val ↔
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝.val
Theorem: Arith.HSemiformula.ProperOn.rew
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝¹.val ↔
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝.val
Tactic:
exact h.iff _
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.rew
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
n₁ m n₂ : ℕ
p : HSemiformula L M n₁ (𝚫, m)
h : ProperWithParamOn M p
f : Fin n₁ → Semiterm L M n₂
⊢ ProperWithParamOn M (HSemiformula.rew (Rew.substs f) p)
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
⊢ ProperWithParamOn M (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝))
Theorem: Arith.HSemiformula.ProperWithParamOn.rew
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
⊢ ProperWithParamOn M (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝))
Tactic:
intro e
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalm M e id) (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝)).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.rew
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalm M e id) (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝)).pi.val
Tactic:
simp [ProperOn, HSemiformula.rew, Semiformula.eval_rew, Function.comp, h.iff, Empty.eq_elim]
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e id (f x)) fun x => x) a✝¹.val ↔
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e id (f x)) fun x => x) a✝.val
Theorem: Arith.HSemiformula.ProperWithParamOn.rew
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e id (f x)) fun x => x) a✝¹.val ↔
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e id (f x)) fun x => x) a✝.val
Tactic:
exact h.iff _
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_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✝¹ : Structure L M
inst✝ : Structure.ORing L M
Γ : HierarchySymbol
p : HSemiformula ℒₒᵣ ξ n Γ
⊢ (emb L p).val = (Semiformula.lMap Language.oringEmb) 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
Γ : SigmaPiDelta
m : ℕ
p : HSemiformula ℒₒᵣ ξ n (Γ, m)
⊢ (emb L p).val = (Semiformula.lMap Language.oringEmb) p.val
Theorem: Arith.HSemiformula.val_emb
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 : HSemiformula ℒₒᵣ ξ n (Γ, m)
⊢ (emb L p).val = (Semiformula.lMap Language.oringEmb) p.val
Tactic:
rcases p with (_ | _ | ⟨⟨p, _⟩, ⟨q, _⟩⟩) <;> simp [rew, val]
Proof state after:
no goals
Theorem: Arith.HSemiformula.pi_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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
p : HSemiformula ℒₒᵣ ξ n (𝚫, m)
⊢ (emb L p).pi = emb L p.pi
Tactic:
cases 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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ ξ n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ ξ n (𝚷, m)
⊢ (emb L (a✝¹.mkDelta a✝)).pi = emb L (a✝¹.mkDelta a✝).pi
Theorem: Arith.HSemiformula.pi_emb
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ ξ n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ ξ n (𝚷, m)
⊢ (emb L (a✝¹.mkDelta a✝)).pi = emb L (a✝¹.mkDelta a✝).pi
Tactic:
rfl
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
p : HSemiformula ℒₒᵣ ξ n (𝚫, m)
⊢ (emb L p).sigma = emb L p.sigma
Tactic:
cases 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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ ξ n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ ξ n (𝚷, m)
⊢ (emb L (a✝¹.mkDelta a✝)).sigma = emb L (a✝¹.mkDelta a✝).sigma
Theorem: Arith.HSemiformula.sigma_emb
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ ξ n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ ξ n (𝚷, m)
⊢ (emb L (a✝¹.mkDelta a✝)).sigma = emb L (a✝¹.mkDelta a✝).sigma
Tactic:
rfl
Proof state after:
no goals
Theorem: Arith.HSemiformula.emb_proper
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 : (𝚫, m)-Semisentence n
⊢ ProperOn M (emb L p) ↔ ProperOn M p
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ Empty n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ Empty n (𝚷, m)
⊢ ProperOn M (emb L (a✝¹.mkDelta a✝)) ↔ ProperOn M (a✝¹.mkDelta a✝)
Theorem: Arith.HSemiformula.emb_proper
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ Empty n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ Empty n (𝚷, m)
⊢ ProperOn M (emb L (a✝¹.mkDelta a✝)) ↔ ProperOn M (a✝¹.mkDelta a✝)
Tactic:
simp [ProperOn, emb]
Proof state after:
no goals
Theorem: Arith.HSemiformula.emb_properWithParam
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 ℒₒᵣ M n (𝚫, m)
⊢ ProperWithParamOn M (emb L p) ↔ ProperWithParamOn M p
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ M n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ M n (𝚷, m)
⊢ ProperWithParamOn M (emb L (a✝¹.mkDelta a✝)) ↔ ProperWithParamOn M (a✝¹.mkDelta a✝)
Theorem: Arith.HSemiformula.emb_properWithParam
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
a✝¹ : HSemiformula ℒₒᵣ M n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ M n (𝚷, m)
⊢ ProperWithParamOn M (emb L (a✝¹.mkDelta a✝)) ↔ ProperWithParamOn M (a✝¹.mkDelta a✝)
Tactic:
simp [ProperWithParamOn, emb]
Proof state after:
no goals
Theorem: Arith.HSemiformula.eval_extd_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✝¹ : Structure L M
inst✝ : Structure.ORing L M
Γ : HierarchySymbol
e : Fin n → M
ε : ξ → M
p : HSemiformula ℒₒᵣ ξ n Γ
⊢ (Semiformula.Evalm M e ε) (extd L p).val ↔ (Semiformula.Evalm M e ε) p.val
Tactic:
induction p <;> simp [extd, *]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.extd
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 : (𝚫, m)-Semisentence n
h : ProperOn M p
⊢ ProperOn M (HSemiformula.extd L 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
m : ℕ
p : (𝚫, m)-Semisentence n
h : ProperOn M p
e : Fin n → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.extd L p).pi.val
Theorem: Arith.HSemiformula.ProperOn.extd
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 : (𝚫, m)-Semisentence n
h : ProperOn M p
e : Fin n → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.extd L 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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
e : Fin n → M
a✝¹ : HSemiformula ℒₒᵣ Empty n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ Empty n (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).pi.val
Theorem: Arith.HSemiformula.ProperOn.extd
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
e : Fin n → M
a✝¹ : HSemiformula ℒₒᵣ Empty n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ Empty n (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).pi.val
Tactic:
simpa [HSemiformula.extd] using h.iff e
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.extd
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 : (𝚫, m)-Semisentence n
h : ProperOn M p
⊢ ProperOn M (HSemiformula.extd L 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
m : ℕ
p : (𝚫, m)-Semisentence n
h : ProperOn M p
e : Fin n → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.extd L p).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.extd
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 : (𝚫, m)-Semisentence n
h : ProperOn M p
e : Fin n → M
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L p).sigma.val ↔ (Semiformula.Evalbm M e) (HSemiformula.extd L 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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
e : Fin n → M
a✝¹ : HSemiformula ℒₒᵣ Empty n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ Empty n (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).pi.val
Theorem: Arith.HSemiformula.ProperWithParamOn.extd
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✝¹ : Structure L M
inst✝ : Structure.ORing L M
m : ℕ
e : Fin n → M
a✝¹ : HSemiformula ℒₒᵣ Empty n (𝚺, m)
a✝ : HSemiformula ℒₒᵣ Empty n (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalbm M e) (HSemiformula.extd L (a✝¹.mkDelta a✝)).pi.val
Tactic:
simpa [HSemiformula.extd] using h.iff e
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigma_extd_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
m : ℕ
p : HSemiformula ℒₒᵣ ξ n (𝚺, m)
⊢ (extd L p).val = (Semiformula.lMap Language.oringEmb) p.val
Tactic:
rcases p
Proof state after:
case mkSigma
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✝ : Semiformula ℒₒᵣ ξ n
a✝ : Hierarchy 𝚺 m p✝
⊢ (extd L (mkSigma p✝ a✝)).val = (Semiformula.lMap Language.oringEmb) (mkSigma p✝ a✝).val
Theorem: Arith.HSemiformula.sigma_extd_val
Proof state before:
case mkSigma
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✝ : Semiformula ℒₒᵣ ξ n
a✝ : Hierarchy 𝚺 m p✝
⊢ (extd L (mkSigma p✝ a✝)).val = (Semiformula.lMap Language.oringEmb) (mkSigma p✝ a✝).val
Tactic:
simp [extd]
Proof state after:
no goals
Theorem: Arith.HSemiformula.pi_extd_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
m : ℕ
p : HSemiformula ℒₒᵣ ξ n (𝚷, m)
⊢ (extd L p).val = (Semiformula.lMap Language.oringEmb) p.val
Tactic:
rcases p
Proof state after:
case mkPi
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✝ : Semiformula ℒₒᵣ ξ n
a✝ : Hierarchy 𝚷 m p✝
⊢ (extd L (mkPi p✝ a✝)).val = (Semiformula.lMap Language.oringEmb) (mkPi p✝ a✝).val
Theorem: Arith.HSemiformula.pi_extd_val
Proof state before:
case mkPi
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✝ : Semiformula ℒₒᵣ ξ n
a✝ : Hierarchy 𝚷 m p✝
⊢ (extd L (mkPi p✝ a✝)).val = (Semiformula.lMap Language.oringEmb) (mkPi p✝ a✝).val
Tactic:
simp [extd]
Proof state after:
no goals
Theorem: Arith.HSemiformula.sigmaZero
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 : ℕ
Γ : SigmaPiDelta
p : HSemiformula L ξ k (𝚫, 0)
⊢ Hierarchy 𝚺 0 p.val
Tactic:
simpa [val_sigma] using p.sigma.sigma_prop
Proof state after:
no goals
Theorem: Arith.HSemiformula.ofZero_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 : ℕ
Γ' : SigmaPiDelta
p : HSemiformula L ξ k (Γ', 0)
Γ : HierarchySymbol
⊢ (p.ofZero Γ).val = p.val
Tactic:
match Γ with
| (𝚺, _) => simp [ofZero]
| (𝚷, _) => simp [ofZero]
| (𝚫, _) => simp [ofZero]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ofZero_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 : ℕ
Γ' : SigmaPiDelta
p : HSemiformula L ξ k (Γ', 0)
Γ : HierarchySymbol
snd✝ : ℕ
⊢ (p.ofZero (𝚺, snd✝)).val = p.val
Tactic:
simp [ofZero]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ofZero_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 : ℕ
Γ' : SigmaPiDelta
p : HSemiformula L ξ k (Γ', 0)
Γ : HierarchySymbol
snd✝ : ℕ
⊢ (p.ofZero (𝚷, snd✝)).val = p.val
Tactic:
simp [ofZero]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ofZero_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 : ℕ
Γ' : SigmaPiDelta
p : HSemiformula L ξ k (Γ', 0)
Γ : HierarchySymbol
snd✝ : ℕ
⊢ (p.ofZero (𝚫, snd✝)).val = p.val
Tactic:
simp [ofZero]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperOn.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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k : ℕ
Γ' : SigmaPiDelta
p : HSemisentence L k (Γ', 0)
m : ℕ
⊢ ProperOn M (ofZero p (𝚫, m))
Tactic:
simp [ProperOn, ofZero]
Proof state after:
no goals
Theorem: Arith.HSemiformula.ProperWithParamOn.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✝¹ : Structure L M
inst✝ : Structure.ORing L M
k : ℕ
Γ' : SigmaPiDelta
p : HSemiformula L M k (Γ', 0)
m : ℕ
⊢ ProperWithParamOn M (p.ofZero (𝚫, m))
Tactic:
simp [ProperWithParamOn, ofZero]
Proof state after:
no goals
Theorem: Arith.HSemiformula.val_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
Γ : 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 = ⊤