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

State before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
μ₂ : Type u_2
n₂ : ℕ
p : Semiformula L μ₁ n₁
h : StrictHierarchy Γ s p
ω : Rew L μ₁ n₁ μ₂ n₂
⊢ StrictHierarchy Γ s (ω.hom p)
Tactic:
induction h generalizing μ₂ n₂ <;> try simp
State after:
case zero
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
a✝ : DeltaZero p✝
μ₂ : Type u_2
n₂ : ℕ
ω : Rew L μ₁ x✝ μ₂ n₂
⊢ StrictHierarchy Γ✝ s✝ (ω.hom p✝)

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

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

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

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

State before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
h : DeltaZero p✝
μ₂ : Type u_2
n₂ : ℕ
ω : Rew L μ₁ x✝ μ₂ n₂
⊢ StrictHierarchy Γ✝ s✝ (ω.hom p✝)
Tactic:
case zero h => exact zero <| (Hierarchy.rew_iff (ω := ω)).mpr h
State after:
no goals

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

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

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

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

State before:
case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {μ₂ : Type u_2} {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), StrictHierarchy 𝚷 (s✝ + 1) (ω.hom p✝)
μ₂ : Type u_2
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ StrictHierarchy 𝚷 (s✝ + 1) (ω.hom (∀' p✝))
Tactic:
simp
State after:
case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {μ₂ : Type u_2} {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), StrictHierarchy 𝚷 (s✝ + 1) (ω.hom p✝)
μ₂ : Type u_2
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ StrictHierarchy 𝚷 (s✝ + 1) (∀' ω.q.hom p✝)

State before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
h : DeltaZero p✝
μ₂ : Type u_2
n₂ : ℕ
ω : Rew L μ₁ x✝ μ₂ n₂
⊢ StrictHierarchy Γ✝ s✝ (ω.hom p✝)
Tactic:
exact zero <| (Hierarchy.rew_iff (ω := ω)).mpr h
State after:
no goals

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

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

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

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