Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists (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 bex
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 ex
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 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✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p

case dummy_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✝ + 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 bex => 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 ex => 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 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✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
case dummy_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✝ : ℕ
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