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

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

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

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

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

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

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