internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Hierarchy.lt
Proof state before:
L✝ : Language
inst✝² : L✝.LT
μ : Type v
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
n : ℕ
Γ : Polarity
s : ℕ
t u : Semiterm L μ n
⊢ Hierarchy Γ s (“!!t < !!u”)
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂,
  Semiformula.Operator.Eq.sentence_eq, Semiformula.Operator.LT.sentence_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.le
Proof state before:
L✝ : Language
inst✝² : L✝.LT
μ : Type v
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
n : ℕ
Γ : Polarity
s : ℕ
t u : Semiterm L μ n
⊢ Hierarchy Γ s (“!!t ≤ !!u”)
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂,
  Semiformula.Operator.Eq.sentence_eq, Semiformula.Operator.LT.sentence_eq,
  Semiformula.Operator.LE.sentence_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
⊢ Hierarchy Γ s p → Hierarchy Γ.alt s (~p)
Tactic:
intro h
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ.alt s (~p)
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ.alt s (~p)
Tactic:
induction h <;> try simp[*]
Proof state after:
case ball
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : 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✝ : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)

case bex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : 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✝ : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)

case ex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)

case all
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)

case sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
a_ih✝ : Hierarchy 𝚺.alt s✝ (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)

case dummy_sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)
Tactic:
case bex pos _ ih => exact ball pos ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)
Tactic:
case ball pos _ ih => exact bex pos ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
case ex ih => exact all ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
case all ih => exact ex ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
case sigma ih => exact pi ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺.alt s✝ (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
case pi ih => exact sigma ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)
Tactic:
case dummy_pi ih => exact dummy_sigma ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)
Tactic:
case dummy_sigma ih => exact dummy_pi ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷.alt (s✝ + 1 + 1) (~(∃' p✝))
Tactic:
simp[*]
Proof state after:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)
Tactic:
exact ball pos ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)
Tactic:
exact bex pos ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
exact all ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
exact ex ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)
Tactic:
exact pi ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
ih : Hierarchy 𝚺.alt s✝ (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)
Tactic:
exact sigma ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
ih : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)
Tactic:
exact dummy_sigma ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
ih : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)
Tactic:
exact dummy_pi ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s (~p)
⊢ Hierarchy Γ.alt s p
Tactic:
simpa using neg h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.neg_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ.alt s p
⊢ Hierarchy Γ s (~p)
Tactic:
simpa using neg h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.imp_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s (p ⟶ q) ↔ Hierarchy Γ.alt s p ∧ Hierarchy Γ s q
Tactic:
simp[Semiformula.imp_eq]
Proof state after:
no goals
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 (“(∀[#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.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
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.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
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 ball
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 all
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 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✝ 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_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✝ + 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.ball_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 ball p t pt hp ih =>
  rcases hq with ⟨rfl, rfl⟩
  assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ball_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 all hp ih =>
  rcases hq with rfl
  simpa using hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ball_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 pi 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.ball_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_sigma hp _ =>
  rcases hq with rfl
  simp at hp
  exact hp.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ball_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:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ball_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.ball_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.ball_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.ball_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.ball_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.ball_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.ball_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.ball_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.ball_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.ball_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