internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Hierarchy.ball_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
⊢ Hierarchy Γ s p → Hierarchy Γ s (“(∀[#0 < !!t] !p)”)
Tactic:
intro hp
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∀[#0 < !!t] !p)”)
Theorem: LO.FirstOrder.Arith.Hierarchy.ball_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∀[#0 < !!t] !p)”)
Tactic:
exact hp.ball ht
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”) → Hierarchy Γ s p
Tactic:
generalize hq : (∃[“x | x < !!t”] p) = q
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
⊢ Hierarchy Γ s q → Hierarchy Γ s p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
⊢ Hierarchy Γ s q → Hierarchy Γ s p
Tactic:
intro H
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
H : Hierarchy Γ s q
⊢ Hierarchy Γ s p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
q : Semiformula L μ n
hq : (“(∃[#0 < !!t] !p)”) = q
H : Hierarchy Γ s q
⊢ Hierarchy Γ s p
Tactic:
induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hq
Proof state after:
case bex
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy Γ✝ s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p

case ex
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case sigma
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚷 s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy Γ✝ s✝ p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy Γ✝ s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p
Tactic:
case bex p t pt hp ih =>
  rcases hq with ⟨rfl, rfl⟩
  assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
case ex hp ih =>
  rcases hq with rfl
  simpa using hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚷 s p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚷 s p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s + 1) p
Tactic:
case sigma s _ _ hp ih =>
  rcases hq with rfl
  exact (show Hierarchy 𝚷 s p from by simpa using hp).accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
case dummy_pi hp _ =>
  rcases hq with rfl
  simp at hp
  exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(∃[#0 < !!t] !p)”) = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp [LogicalConnective.ball, LogicalConnective.bex] at hq
Proof state after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pt : t✝.Positive
hp : Hierarchy Γ✝ s✝ p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy Γ✝ s✝ p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p
Tactic:
rcases hq with ⟨rfl, rfl⟩
Proof state after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht pt : t.Positive
hp : Hierarchy Γ✝ s✝ p
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p_1)”) = p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht pt : t.Positive
hp : Hierarchy Γ✝ s✝ p
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p_1)”) = p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
rcases hq with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1) p
Tactic:
simpa using hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚷 s p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚷 s p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚺 (s + 1) p
Tactic:
rcases hq with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 s (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚷 s p_1
⊢ Hierarchy 𝚺 (s + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 s (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚷 s p_1
⊢ Hierarchy 𝚺 (s + 1) p
Tactic:
exact (show Hierarchy 𝚷 s p from by simpa using hp).accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 s (“(#0 < !!t ∧ !p)”)
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚷 s p_1
⊢ Hierarchy 𝚷 s p
Tactic:
simpa using hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
rcases hq with rfl
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚺 (s✝ + 1) (“(#0 < !!t ∧ !p)”)
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
simp at hp
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∃[#0 < !!t_1] !p_1)”) = (“(#0 < !!t ∧ !p)”) → Hierarchy 𝚺 (s✝ + 1) p_1
hp : Hierarchy 𝚺 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
Tactic:
exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
⊢ Hierarchy Γ s p → Hierarchy Γ s (“(∃[#0 < !!t] !p)”)
Tactic:
intro hp
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”)
Theorem: LO.FirstOrder.Arith.Hierarchy.bex_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”)
Tactic:
exact hp.bex ht
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ballLT_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ n
⊢ Hierarchy Γ s (Semiformula.ballLT t p) ↔ Hierarchy Γ s p
Tactic:
simp [Semiformula.ballLT]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bexLT_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ n
⊢ Hierarchy Γ s (Semiformula.bexLT t p) ↔ Hierarchy Γ s p
Tactic:
simp [Semiformula.bexLT]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ballLTSucc_iff
Proof state before:
L : Language
inst✝³ : L.LT
μ : Type v
inst✝² : L.Zero
inst✝¹ : L.One
inst✝ : L.Add
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ n
⊢ Hierarchy Γ s (Semiformula.ballLTSucc t p) ↔ Hierarchy Γ s p
Tactic:
simp [Semiformula.ballLTSucc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bexLTSucc_iff
Proof state before:
L : Language
inst✝³ : L.LT
μ : Type v
inst✝² : L.Zero
inst✝¹ : L.One
inst✝ : L.Add
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ n
⊢ Hierarchy Γ s (Semiformula.bexLTSucc t p) ↔ Hierarchy Γ s p
Tactic:
simp [Semiformula.bexLTSucc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
⊢ Hierarchy 𝚷 s (∀' p) → Hierarchy 𝚷 s p
Tactic:
generalize hr : ∀' p = r
Proof state after:
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
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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 ball
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 all
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 pi
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_sigma
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.pi_of_pi_all
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 ball => rcases hr with rfl; simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
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 all => rcases hr with rfl; simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
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 pi hp => rcases hr with rfl; exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
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_sigma hp => rcases hr with rfl; exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
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:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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.pi_of_pi_all
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.sigma_of_sigma_ex
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
⊢ Hierarchy 𝚺 s (∃' p) → Hierarchy 𝚺 s p
Tactic:
generalize hr : ∃' p = r
Proof state after:
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