Theorem: Arith.HSemiformula.ProperOn.rew (Arithmetization/Definability/Hierarchy.lean)

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
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✝))

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]
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

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
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

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 _
State after:
no goals