Theorem: Arith.HSemiformula.ProperWithParamOn.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 : 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
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✝))

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

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

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