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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p → Hierarchy Γ.alt 0 p
Tactic:
generalize hz : 0 = z
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : 0 = z
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : 0 = z
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
Tactic:
rw[eq_comm] at hz
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
Tactic:
intro h
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
h : Hierarchy Γ z p
⊢ Hierarchy Γ.alt z p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
h : Hierarchy Γ z p
⊢ Hierarchy Γ.alt z p
Tactic:
induction h <;> try simp at hz ⊢
State after:
case and
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝

case or
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝

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

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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
ihq : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝
Tactic:
case and _ _ ihp ihq =>
  exact ⟨ihp hz, ihq hz⟩
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
ihq : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝
Tactic:
case or _ _ ihp ihq => exact ⟨ihp hz, ihq hz⟩
State after:
no goals

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

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

State before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : s✝ + 1 = 0 → Hierarchy 𝚺.alt (s✝ + 1) p✝
hz : s✝ + 1 + 1 = 0
⊢ Hierarchy 𝚷.alt (s✝ + 1 + 1) (∃' p✝)
Tactic:
simp at hz ⊢
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
ihq : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝
Tactic:
exact ⟨ihp hz, ihq hz⟩
State after:
no goals

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

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