Theorem: LO.FirstOrder.Arith.Hierarchy.accum (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∀' p✝)
Tactic:
cases Γ
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)

State before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact hp.dummy_sigma
State after:
no goals

State before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact (hp.accum 𝚷).all
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∃' p✝)
Tactic:
cases Γ
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)

State before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact (hp.accum 𝚺).ex
State after:
no goals

State before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact hp.dummy_pi
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∃' p✝)
Tactic:
cases Γ
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)

State before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact ((hp.accum 𝚺).accum 𝚺).ex
State after:
no goals

State before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact (hp.accum 𝚺).dummy_pi
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∀' p✝)
Tactic:
cases Γ
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)

State before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact (hp.accum 𝚷).dummy_sigma
State after:
no goals

State before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact ((hp.accum 𝚷).accum 𝚷).all
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1 + 1) (∀' p✝)
Tactic:
cases Γ
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∀' p✝)

State before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∀' p✝)
Tactic:
exact (hp.accum 𝚷).dummy_sigma
State after:
no goals

State before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∀' p✝)
Tactic:
exact ((hp.accum 𝚷).accum 𝚷).all
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1 + 1) (∃' p✝)
Tactic:
cases Γ
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∃' p✝)

State before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∃' p✝)
Tactic:
exact ((hp.accum 𝚺).accum 𝚺).ex
State after:
no goals

State before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∃' p✝)
Tactic:
exact (hp.accum 𝚺).dummy_pi
State after:
no goals