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

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
⊢ Hierarchy b s (∀' p) → Hierarchy b s p
Tactic:
intro h
State after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∀' p)
⊢ Hierarchy b s p

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∀' p)
⊢ Hierarchy b s p
Tactic:
rcases h
State after:
case ball
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)

case all
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p

case pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p

case dummy_sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)
Tactic:
case ball => simpa
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
case all => assumption
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
case pi h => exact h.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
Tactic:
case dummy_sigma h => exact h.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)
Tactic:
simpa
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
assumption
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
exact h.accum _
State after:
no goals

State before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
Tactic:
exact h.accum _
State after:
no goals