internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof 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✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof 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✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
⊢ StrictHierarchy Γ s (ω.hom p) → StrictHierarchy Γ s p
Tactic:
generalize hq : ω.hom p = q
Proof state after:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
q : Semiformula L μ₂ n₂
hq : ω.hom p = q
⊢ StrictHierarchy Γ s q → StrictHierarchy Γ s p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
q : Semiformula L μ₂ n₂
hq : ω.hom p = q
⊢ StrictHierarchy Γ s q → StrictHierarchy Γ s p
Tactic:
intro h
Proof state after:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
q : Semiformula L μ₂ n₂
hq : ω.hom p = q
h : StrictHierarchy Γ s q
⊢ StrictHierarchy Γ s p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
q : Semiformula L μ₂ n₂
hq : ω.hom p = q
h : StrictHierarchy Γ s q
⊢ StrictHierarchy Γ s p
Tactic:
induction h generalizing n₁ <;> try simp [Rew.eq_ball_iff, Rew.eq_bex_iff, Rew.eq_all_iff, Rew.eq_ex_iff] at hq ⊢
Proof state after:
case zero
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₂ x✝
a✝ : DeltaZero p✝
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
hq : ω.hom p = p✝
⊢ StrictHierarchy Γ✝ s✝ p

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

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

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

case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q✝ : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
q : Semiformula L μ₂ x✝
h : DeltaZero q
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
hq : ω.hom p = q
⊢ StrictHierarchy Γ✝ s✝ p
Tactic:
case zero q h =>
  rcases hq; exact zero (Hierarchy.rew_iff.mp h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚷 s✝ p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ StrictHierarchy 𝚺 (s✝ + 1) p
Tactic:
case sigma h ih =>
  rcases hq with ⟨_, rfl, rfl⟩
  exact (ih ω.q rfl).sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚺 s✝ p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Tactic:
case pi h ih =>
  rcases hq with ⟨_, rfl, rfl⟩
  exact (ih ω.q rfl).pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚺 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ StrictHierarchy 𝚺 (s✝ + 1) p
Tactic:
case ex h ih =>
  rcases hq with ⟨_, rfl, rfl⟩
  exact (ih ω.q rfl).ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Tactic:
case all ih =>
  rcases hq with ⟨_, rfl, rfl⟩
  exact (ih ω.q rfl).all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ω.hom p = ∀' p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Tactic:
simp [Rew.eq_ball_iff, Rew.eq_bex_iff, Rew.eq_all_iff, Rew.eq_ex_iff] at hq ⊢
Proof state after:
case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q✝ : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
q : Semiformula L μ₂ x✝
h : DeltaZero q
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
hq : ω.hom p = q
⊢ StrictHierarchy Γ✝ s✝ p
Tactic:
rcases hq
Proof state after:
case refl
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
h : DeltaZero (ω.hom p)
⊢ StrictHierarchy Γ✝ s✝ p
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
case refl
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
h : DeltaZero (ω.hom p)
⊢ StrictHierarchy Γ✝ s✝ p
Tactic:
exact zero (Hierarchy.rew_iff.mp h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚷 s✝ p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ StrictHierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hq with ⟨_, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚷 s✝ (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚷 s✝ p
⊢ StrictHierarchy 𝚺 (s✝ + 1) (∃' w✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚷 s✝ (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚷 s✝ p
⊢ StrictHierarchy 𝚺 (s✝ + 1) (∃' w✝)
Tactic:
exact (ih ω.q rfl).sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚺 s✝ p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Tactic:
rcases hq with ⟨_, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚺 s✝ (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚺 s✝ p
⊢ StrictHierarchy 𝚷 (s✝ + 1) (∀' w✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚺 s✝ (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚺 s✝ p
⊢ StrictHierarchy 𝚷 (s✝ + 1) (∀' w✝)
Tactic:
exact (ih ω.q rfl).pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚺 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ StrictHierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hq with ⟨_, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚺 (s✝ + 1) (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚺 (s✝ + 1) p
⊢ StrictHierarchy 𝚺 (s✝ + 1) (∃' w✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚺 (s✝ + 1) (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚺 (s✝ + 1) p
⊢ StrictHierarchy 𝚺 (s✝ + 1) (∃' w✝)
Tactic:
exact (ih ω.q rfl).ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
Tactic:
rcases hq with ⟨_, rfl, rfl⟩
Proof state after:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚷 (s✝ + 1) p
⊢ StrictHierarchy 𝚷 (s✝ + 1) (∀' w✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.rew_iff
Proof state before:
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚷 (s✝ + 1) p
⊢ StrictHierarchy 𝚷 (s✝ + 1) (∀' w✝)
Tactic:
exact (ih ω.q rfl).all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
h : StrictHierarchy Γ s p
⊢ StrictHierarchy Γ (s + 1) p
Tactic:
induction h
Proof state after:
case zero
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
a✝ : DeltaZero p✝
⊢ StrictHierarchy Γ✝ (s✝ + 1) p✝

case sigma
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 s✝ p✝
a_ih✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
⊢ StrictHierarchy 𝚺 (s✝ + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 s✝ p✝
a_ih✝ : StrictHierarchy 𝚺 (s✝ + 1) p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1 + 1) (∀' p✝)

case ex
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : StrictHierarchy 𝚺 (s✝ + 1 + 1) p✝
⊢ StrictHierarchy 𝚺 (s✝ + 1 + 1) (∃' p✝)

case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : StrictHierarchy 𝚷 (s✝ + 1 + 1) p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1 + 1) (∀' p✝)
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
h : DeltaZero p✝
⊢ StrictHierarchy Γ✝ (s✝ + 1) p✝
Tactic:
case zero h => exact zero h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 s✝ p✝
ih : StrictHierarchy 𝚷 (s✝ + 1) p✝
⊢ StrictHierarchy 𝚺 (s✝ + 1 + 1) (∃' p✝)
Tactic:
case sigma ih => exact ih.sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.StrictHierarchy.succ
Proof state before:
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ s : ℕ
Γ : Polarity
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 s✝ p✝
ih : StrictHierarchy 𝚺 (s✝ + 1) p✝
⊢ StrictHierarchy 𝚷 (s✝ + 1 + 1) (∀' p✝)
Tactic:
case pi ih => exact ih.pi
Proof state after:
no goals