internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
⊢ Hierarchy 𝚺 s r → Hierarchy 𝚺 s p
Tactic:
generalize hb : (𝚺 : Polarity) = Γ
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
⊢ Hierarchy Γ s r → Hierarchy Γ s p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
⊢ Hierarchy Γ s r → Hierarchy Γ s p
Tactic:
intro H
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∃' p = r
Γ : Polarity
hb : 𝚺 = Γ
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p
Tactic:
cases H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
Proof state after:
case bex
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
hr : p = (“(#0 < !!t✝ ∧ !p✝)”)
⊢ Hierarchy Γ s p

case ex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
hr : p = (“(#0 < !!t✝ ∧ !p✝)”)
⊢ Hierarchy Γ s p
Tactic:
case bex => rcases hr with rfl; simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case ex => rcases hr with rfl; simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case sigma hp => rcases hr with rfl; exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
case dummy_pi hp => rcases hr with rfl; exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : ∃' p = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hr
Proof state after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
hr : p = (“(#0 < !!t✝ ∧ !p✝)”)
⊢ Hierarchy Γ s p
Tactic:
rcases hr with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
⊢ Hierarchy Γ s (“(#0 < !!t✝ ∧ !p✝)”)
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
Γ : Polarity
hb : 𝚺 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
⊢ Hierarchy Γ s (“(#0 < !!t✝ ∧ !p✝)”)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hr with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hr with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
hp : Hierarchy 𝚷 s✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚺
hp : Hierarchy 𝚷 s✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
rcases hr with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚺 = 𝚷
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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]
Proof 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✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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 _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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 _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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]
Proof 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✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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 _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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 _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.rew
Proof 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
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
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ Hierarchy Γ s (ω.hom p) ↔ Hierarchy Γ s p
Tactic:
constructor
Proof state after:
case mp
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 (ω.hom p) → Hierarchy Γ s p

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)
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case mp
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 (ω.hom p) → Hierarchy Γ s p
Tactic:
generalize eq : ω.hom p = q
Proof state after:
case mp
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₁
q : Semiformula L μ₂ n₂
eq : ω.hom p = q
⊢ Hierarchy Γ s q → Hierarchy Γ s p
Theorem: LO.FirstOrder.Arith.Hierarchy.rew_iff
Proof state before:
case mp
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₁
q : Semiformula L μ₂ n₂
eq : ω.hom p = q
⊢ Hierarchy Γ s q → Hierarchy Γ s p
Tactic:
intro hq
Proof state after:
case mp
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₁
q : Semiformula L μ₂ n₂
eq : ω.hom p = q
hq : Hierarchy Γ s q
⊢ 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✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : p = ⊤
⊢ Hierarchy Γ✝ s✝ p
Tactic:
case verum => rcases eq with rfl; 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:
case falsum => rcases eq with rfl; 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:
case rel => rcases eq with ⟨v', rfl, rfl⟩; 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:
case nrel => rcases eq with ⟨v', rfl, rfl⟩; 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:
case and ihp ihq =>
  rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
  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:
case or ihp ihq =>
  rcases eq with ⟨p₁, rfl, p₂, rfl, rfl⟩
  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:
case ball pos _ ih =>
  simp [Rew.eq_lt_iff] at eq
  rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
  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✝ : ℕ
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:
case bex pos _ ih =>
  simp [Rew.eq_lt_iff] at eq
  rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
  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:
case all ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  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:
case ex ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  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:
case pi ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  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:
case sigma ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  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:
case dummy_sigma ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  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:
case dummy_pi ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).dummy_pi
Proof state after:
no goals