Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all (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 ball
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 all
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 pi
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_sigma
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 ball => 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 all => 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 pi 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_sigma 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:
no goals

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