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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
⊢ Hierarchy Γ s p → Hierarchy Γ.alt s (~p)
Tactic:
intro h
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ.alt s (~p)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ.alt s (~p)
Tactic:
induction h <;> try simp[*]
State after:
case ball
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)

case bex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)

case ex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)

case all
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)

case sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)

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

case dummy_sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)
Tactic:
case bex pos _ ih => exact ball pos ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)
Tactic:
case ball pos _ ih => exact bex pos ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
case ex ih => exact all ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
case all ih => exact ex ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
case sigma ih => exact pi ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺.alt s✝ (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
case pi ih => exact sigma ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)
Tactic:
case dummy_pi ih => exact dummy_sigma ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)
Tactic:
case dummy_sigma ih => exact dummy_pi ih
State after:
no goals

State before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷.alt (s✝ + 1 + 1) (~(∃' p✝))
Tactic:
simp[*]
State after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)
Tactic:
exact ball pos ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)
Tactic:
exact bex pos ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
exact all ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
exact ex ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
exact pi ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺.alt s✝ (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
exact sigma ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)
Tactic:
exact dummy_sigma ih
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)
Tactic:
exact dummy_pi ih
State after:
no goals