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

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ Hierarchy Γ s p → Hierarchy Γ s (ω.hom p)
Tactic:
intro h
State after:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
h : Hierarchy Γ s p
⊢ Hierarchy Γ s (ω.hom p)

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
h : Hierarchy Γ s p
⊢ Hierarchy Γ s (ω.hom p)
Tactic:
induction h generalizing n₂ <;> try simp [*, Rew.rel,Rew.nrel]
State after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
a_ih✝ : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p✝)

case dummy_sigma
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ω.q.hom p✝)

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ω.q.hom p✝)

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p✝)
Tactic:
case sigma ih => exact (ih _).accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p✝)
Tactic:
case pi ih => exact (ih _).accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ω.q.hom p✝)
Tactic:
case dummy_pi ih => exact (ih _).dummy_pi
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ω.q.hom p✝)
Tactic:
case dummy_sigma ih => exact (ih _).dummy_sigma
State after:
no goals

State before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (ω.hom (∃' p✝))
Tactic:
simp [*, Rew.rel,Rew.nrel]
State after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ω.q.hom p✝)

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p✝)
Tactic:
exact (ih _).accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p✝)
Tactic:
exact (ih _).accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚺 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ω.q.hom p✝)
Tactic:
exact (ih _).dummy_pi
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 (s✝ + 1) (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ω.q.hom p✝)
Tactic:
exact (ih _).dummy_sigma
State after:
no goals