internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case mp.dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ω.hom p = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp [Rew.eq_rel_iff, Rew.eq_nrel_iff, Rew.eq_ball_iff, Rew.eq_bex_iff, Rew.eq_all_iff, Rew.eq_ex_iff] at eq
Proof state after:
case mp.dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : p = ⊤
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
⊢ Hierarchy Γ✝ s✝ ⊤
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
⊢ Hierarchy Γ✝ s✝ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : p = ⊥
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
⊢ Hierarchy Γ✝ s✝ ⊥
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
⊢ Hierarchy Γ✝ s✝ ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ₂ x✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
p : Semiformula L μ₁ n₁
eq : ∃ v', ⇑ω ∘ v' = v✝ ∧ p = Semiformula.rel r✝ v'
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨v', rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.rel r✝ v')
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.rel r✝ v')
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ₂ x✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
p : Semiformula L μ₁ n₁
eq : ∃ v', ⇑ω ∘ v' = v✝ ∧ p = Semiformula.nrel r✝ v'
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨v', rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.nrel r✝ v')
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
v' : Fin k✝ → Semiterm L μ₁ n₁
⊢ Hierarchy Γ✝ s✝ (Semiformula.nrel r✝ v')
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ₂ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = q✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.hom p₁ = p✝ ∧ ∃ x, ω.hom x = q✝ ∧ p = p₁ ⋏ x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p₁ : Semiformula L μ₁ n₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋏ p₂)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p₁ : Semiformula L μ₁ n₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋏ p₂)
Tactic:
simpa using ⟨ihp rfl, ihq rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ₂ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = q✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.hom p₁ = p✝ ∧ ∃ x, ω.hom x = q✝ ∧ p = p₁ ⋎ x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p₁ : Semiformula L μ₁ n₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋎ p₂)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p₁ : Semiformula L μ₁ n₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋎ p₂)
Tactic:
simpa using ⟨ihp rfl, ihq rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.q.hom p₁ = (“#0 < !!t✝”) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
simp [Rew.eq_lt_iff] at eq
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro.refl.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∀[#0 < !!u] !p)”)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro.intro.intro.refl.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∀[#0 < !!u] !p)”)
Tactic:
simpa [show u.Positive from by simpa using pos] using ih rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ u.Positive
Tactic:
simpa using pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.q.hom p₁ = (“#0 < !!t✝”) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∃[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
simp [Rew.eq_lt_iff] at eq
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∃[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∃[p₁] x
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro.refl.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∃[#0 < !!u] !p)”)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro.intro.intro.refl.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∃[#0 < !!u] !p)”)
Tactic:
simpa [show u.Positive from by simpa using pos] using ih rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)
Tactic:
exact (ih rfl).all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)
Tactic:
exact (ih rfl).ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 s✝ p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 s✝ p_1
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' p)
Tactic:
exact (ih rfl).pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 s✝ p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 s✝ p_1
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' p)
Tactic:
exact (ih rfl).sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' p)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' p)
Tactic:
exact (ih rfl).dummy_sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
rcases eq with ⟨p, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' p)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' p)
Tactic:
exact (ih rfl).dummy_pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case mpr
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:
exact rew _
Proof state after:
no goals