internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Hierarchy.exClosure
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
s n : ℕ
p : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s + 1) p
⊢ Hierarchy 𝚺 (s + 1) (∃* p)
Tactic:
simpa using exClosure (hp.ex)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.of_open
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
⊢ p.Open → Hierarchy Γ s p
Tactic:
induction p using Semiformula.rec' <;> simp
Proof state after:
case hand
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : p✝.Open → Hierarchy Γ s p✝
a✝ : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝

case hor
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : p✝.Open → Hierarchy Γ s p✝
a✝ : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Theorem: LO.FirstOrder.Arith.Hierarchy.of_open
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
case hand ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.of_open
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
case hor ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.of_open
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
intro hp hq
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
hp : p✝.Open
hq : q✝.Open
⊢ Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Theorem: LO.FirstOrder.Arith.Hierarchy.of_open
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
hp : p✝.Open
hq : q✝.Open
⊢ Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
Tactic:
exact ⟨ihp hp, ihq hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
⊢ Hierarchy Γ s p → Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)
Tactic:
intro h
Proof state after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)
Tactic:
induction h <;> try simp [*, Semiformula.lMap_rel, Semiformula.lMap_nrel]
Proof state after:
case sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : Hierarchy 𝚷 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)

case pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
a_ih✝ : Hierarchy 𝚺 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)

case dummy_sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' (Semiformula.lMap Language.oringEmb) p✝)

case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case sigma ih => exact ih.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case pi ih => exact ih.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case dummy_pi ih => exact ih.dummy_pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
case dummy_sigma ih => exact ih.dummy_sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) ((Semiformula.lMap Language.oringEmb) (∃' p✝))
Tactic:
simp [*, Semiformula.lMap_rel, Semiformula.lMap_nrel]
Proof state after:
case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺 s✝ ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.dummy_pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.oringEmb
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
s✝ n✝ : ℕ
p✝ : Semiformula ℒₒᵣ μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷 (s✝ + 1) ((Semiformula.lMap Language.oringEmb) p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' (Semiformula.lMap Language.oringEmb) p✝)
Tactic:
exact ih.dummy_sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.iff_iff
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy b s (p ⟷ q) ↔ Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q
Tactic:
simp[Semiformula.iff_eq]
Proof state after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ (Hierarchy b.alt s p ∧ Hierarchy b s q) ∧ Hierarchy b.alt s q ∧ Hierarchy b s p ↔
    Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q
Theorem: LO.FirstOrder.Arith.Hierarchy.iff_iff
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ (Hierarchy b.alt s p ∧ Hierarchy b s q) ∧ Hierarchy b.alt s q ∧ Hierarchy b s p ↔
    Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.iff_iff₀
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
p q : Semiformula L μ n
⊢ Hierarchy b 0 (p ⟷ q) ↔ Hierarchy b 0 p ∧ Hierarchy b 0 q
Tactic:
simp[Semiformula.iff_eq]
Proof state after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
p q : Semiformula L μ n
⊢ Hierarchy b 0 p → Hierarchy b 0 q → Hierarchy b 0 q ∧ Hierarchy b 0 p
Theorem: LO.FirstOrder.Arith.Hierarchy.iff_iff₀
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
p q : Semiformula L μ n
⊢ Hierarchy b 0 p → Hierarchy b 0 q → Hierarchy b 0 q ∧ Hierarchy b 0 p
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.matrix_conj_iff
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
m : ℕ
ξ : Type u_1
b : Polarity
s n : ℕ
p : Fin m → Semiformula L ξ n
⊢ Hierarchy b s (Matrix.conj fun j => p j) ↔ ∀ (j : Fin m), Hierarchy b s (p j)
Tactic:
cases m <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
⊢ Hierarchy b s (∀' p) → Hierarchy b s p
Tactic:
intro h
Proof state after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∀' p)
⊢ Hierarchy b s p
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∀' p)
⊢ Hierarchy b s p
Tactic:
rcases h
Proof state after:
case ball
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)

case all
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p

case pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p

case dummy_sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)
Tactic:
case ball => simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
case all => assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
case pi h => exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
Tactic:
case dummy_sigma h => exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p
Tactic:
exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_forall
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
Tactic:
exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
⊢ Hierarchy b s (∃' p) → Hierarchy b s p
Tactic:
intro h
Proof state after:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∃' p)
⊢ Hierarchy b s p
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∃' p)
⊢ Hierarchy b s p
Tactic:
rcases h
Proof state after:
case bex
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ ∧ !p✝)”)

case ex
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p

case sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 s✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p

case dummy_pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ ∧ !p✝)”)
Tactic:
case bex => simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case ex => assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 s✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case sigma h => exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
case dummy_pi h => exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ ∧ !p✝)”)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 s✝ p
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.remove_exists
Proof state before:
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
exact h.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.consistent_of_sigmaOneSound
Proof state before:
L✝ : Language
inst✝⁵ : L✝.LT
μ : Type v
L : Language
inst✝⁴ : (k : ℕ) → DecidableEq (L.Func k)
inst✝³ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝² : L.LT
inst✝¹ : Structure L ℕ
T : Theory L
inst✝ : SigmaOneSound T
⊢ ⊥ ∈ Hierarchy 𝚺 1
Tactic:
simp [Set.mem_def]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.serial_def
Proof state before:
α : Sort ?u.505
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 0, m := 1, n := 1 } F ↔ Serial F.Rel
Tactic:
simp [GeachConfluent, Symmetric]
Proof state after:
α : Sort ?u.505
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x : F.World}, ∃ u, x ≺ u) ↔ Serial F.Rel
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.serial_def
Proof state before:
α : Sort ?u.505
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x : F.World}, ∃ u, x ≺ u) ↔ Serial F.Rel
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.reflexive_def
Proof state before:
α : Sort ?u.8600
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 0, m := 1, n := 0 } F ↔ Reflexive F.Rel
Tactic:
simp [GeachConfluent, Reflexive]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.symmetric_def
Proof state before:
α : Sort ?u.13729
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 1, m := 0, n := 1 } F ↔ Symmetric F.Rel
Tactic:
simp [GeachConfluent, Symmetric]
Proof state after:
α : Sort ?u.13729
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z ≺ y) ↔ ∀ ⦃x y : F.World⦄, F.Rel x y → F.Rel y x
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.symmetric_def
Proof state before:
α : Sort ?u.13729
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z ≺ y) ↔ ∀ ⦃x y : F.World⦄, F.Rel x y → F.Rel y x
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.transitive_def
Proof state before:
α : Sort ?u.51487
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 2, m := 1, n := 0 } F ↔ Transitive F.Rel
Tactic:
simp [GeachConfluent, Transitive]
Proof state after:
α : Sort ?u.51487
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → ∀ (x_1 : F.World), x ≺ x_1 → x_1 ≺ z → y ≺ z) ↔
    ∀ ⦃x y z : F.World⦄, F.Rel x y → F.Rel y z → F.Rel x z
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.transitive_def
Proof state before:
α : Sort ?u.51487
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → ∀ (x_1 : F.World), x ≺ x_1 → x_1 ≺ z → y ≺ z) ↔
    ∀ ⦃x y z : F.World⦄, F.Rel x y → F.Rel y z → F.Rel x z
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.euclidean_def
Proof state before:
α : Sort ?u.119900
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 1, j := 1, m := 0, n := 1 } F ↔ Euclidean F.Rel
Tactic:
simp [GeachConfluent, Euclidean]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.confluent_def
Proof state before:
α : Sort ?u.131365
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 1, j := 1, m := 1, n := 1 } F ↔ Confluent F.Rel
Tactic:
simp [GeachConfluent, Confluent]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ GeachConfluent { i := 0, j := 1, m := 0, n := 0 } F ↔ Extensive F.Rel
Tactic:
simp [GeachConfluent, Extensive]
Proof state after:
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) ↔ ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) ↔ ∀ ⦃x y : F.World⦄, F.Rel x y → x = y
Tactic:
constructor
Proof state after:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y

case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Theorem: LO.Modal.Standard.Kripke.GeachConfluent.extensive_def
Proof state before:
case mp
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ {x y z : F.World}, x = y → x ≺ z → z = y) → ∀ ⦃x y : F.World⦄, F.Rel x y → x = y

case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y
Tactic:
. intro h x y hyz;
  have := h rfl hyz;
  subst this;
  trivial;
Proof state after:
case mpr
α : Sort ?u.151906
inst✝ : Inhabited α
F : Frame
⊢ (∀ ⦃x y : F.World⦄, F.Rel x y → x = y) → ∀ {x y z : F.World}, x = y → x ≺ z → z = y