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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
⊢ Hierarchy 𝚺 s (∃' p) → Hierarchy 𝚺 s p
Tactic:
generalize hr : ∃' p = r
State after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
⊢ Hierarchy 𝚺 s r → Hierarchy 𝚺 s p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
⊢ Hierarchy 𝚺 s r → Hierarchy 𝚺 s p
Tactic:
generalize hb : (𝚺 : Polarity) = Γ
State after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
⊢ Hierarchy Γ s r → Hierarchy Γ s p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
⊢ Hierarchy Γ s r → Hierarchy Γ s p
Tactic:
intro H
State after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p
Tactic:
cases H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
State after:
case bex
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
hr : p = (“(#0 < !!t✝ ∧ !p✝)”)
⊢ Hierarchy Γ s p

case ex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
hr : p = (“(#0 < !!t✝ ∧ !p✝)”)
⊢ Hierarchy Γ s p
Tactic:
case bex => rcases hr with rfl; simpa
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case ex => rcases hr with rfl; simpa
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case sigma hp => rcases hr with rfl; exact hp.accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
case dummy_pi hp => rcases hr with rfl; exact hp.accum _
State after:
no goals

State before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : ∃' p = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hr
State after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
hr : p = (“(#0 < !!t✝ ∧ !p✝)”)
⊢ Hierarchy Γ s p
Tactic:
rcases hr with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
⊢ Hierarchy Γ s (“(#0 < !!t✝ ∧ !p✝)”)

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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hr with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
simpa
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hr with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
hp : Hierarchy 𝚷 s✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p

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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
rcases hr with rfl
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p

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