internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋎ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋎ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q → Hierarchy Γ s (p ⋎ q)
Tactic:
rintro ⟨hp, hq⟩
Proof state after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋎ q)
Theorem: LO.FirstOrder.Arith.Hierarchy.or_iff
Proof state before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋎ q)
Tactic:
exact Hierarchy.or hp hq
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
m n : ℕ
Γ : Polarity
s : ℕ
p : Fin m → Semiformula L μ n
⊢ Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin m), Hierarchy Γ s (p i)
Tactic:
induction m <;> simp[Matrix.conj, Matrix.vecTail, *]
Proof state after:
case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) ↔ ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff
Proof state before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) ↔ ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
Tactic:
exact ⟨by rintro ⟨hz, hs⟩ i; cases i using Fin.cases <;> simp[*],
       by intro h; exact ⟨h 0, fun _ => h _⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) → ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
Tactic:
rintro ⟨hz, hs⟩ i
Proof state after:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
hz : Hierarchy Γ s (p 0)
hs : ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
i : Fin (n✝ + 1)
⊢ Hierarchy Γ s (p i)
Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff
Proof state before:
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
hz : Hierarchy Γ s (p 0)
hs : ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
i : Fin (n✝ + 1)
⊢ Hierarchy Γ s (p i)
Tactic:
cases i using Fin.cases <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
⊢ (∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)) → Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
Tactic:
intro h
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
h : ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
⊢ Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
Theorem: LO.FirstOrder.Arith.Hierarchy.conj_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
h : ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)
⊢ Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
Tactic:
exact ⟨h 0, fun _ => h _⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p → Hierarchy Γ.alt 0 p
Tactic:
generalize hz : 0 = z
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : 0 = z
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : 0 = z
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
Tactic:
rw[eq_comm] at hz
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
Tactic:
intro h
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
h : Hierarchy Γ z p
⊢ Hierarchy Γ.alt z p
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
h : Hierarchy Γ z p
⊢ Hierarchy Γ.alt z p
Tactic:
induction h <;> try simp at hz ⊢
Proof state after:
case and
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝

case or
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝

case ball
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !p✝)”)

case bex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !p✝)”)
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
ihq : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝
Tactic:
case and _ _ ihp ihq =>
  exact ⟨ihp hz, ihq hz⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
ihq : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝
Tactic:
case or _ _ ihp ihq => exact ⟨ihp hz, ihq hz⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !p✝)”)
Tactic:
case ball pos _ ih => exact ball pos (ih hz)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !p✝)”)
Tactic:
case bex pos _ ih => exact bex pos (ih hz)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : s✝ + 1 = 0 → Hierarchy 𝚺.alt (s✝ + 1) p✝
hz : s✝ + 1 + 1 = 0
⊢ Hierarchy 𝚷.alt (s✝ + 1 + 1) (∃' p✝)
Tactic:
simp at hz ⊢
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
ihq : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝
Tactic:
exact ⟨ihp hz, ihq hz⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !p✝)”)
Tactic:
exact ball pos (ih hz)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !p✝)”)
Tactic:
exact bex pos (ih hz)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ Γ' : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ Hierarchy Γ' 0 p
Tactic:
rcases Γ <;> rcases Γ' <;> simp[pi_zero_iff_sigma_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_iff_delta_zero
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ DeltaZero p
Tactic:
simp[DeltaZero, pi_zero_iff_sigma_zero]
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ Hierarchy 𝚺 0 p
Theorem: LO.FirstOrder.Arith.Hierarchy.zero_iff_delta_zero
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ Hierarchy 𝚺 0 p
Tactic:
apply zero_iff
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.alt_zero_iff_zero
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ.alt 0 p ↔ Hierarchy Γ 0 p
Tactic:
rcases Γ <;> simp[pi_zero_iff_sigma_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∀' p✝)
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact hp.dummy_sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact (hp.accum 𝚷).all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∃' p✝)
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact (hp.accum 𝚺).ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact hp.dummy_pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∃' p✝)
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact ((hp.accum 𝚺).accum 𝚺).ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∃' p✝)
Tactic:
exact (hp.accum 𝚺).dummy_pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∀' p✝)
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact (hp.accum 𝚷).dummy_sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)
Tactic:
exact ((hp.accum 𝚷).accum 𝚷).all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1 + 1) (∀' p✝)
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∀' p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∀' p✝)
Tactic:
exact (hp.accum 𝚷).dummy_sigma
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∀' p✝)
Tactic:
exact ((hp.accum 𝚷).accum 𝚷).all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1 + 1) (∃' p✝)
Tactic:
cases Γ
Proof state after:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∃' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∃' p✝)
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∃' p✝)
Tactic:
exact ((hp.accum 𝚺).accum 𝚺).ex
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.accum
Proof state before:
case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1 + 1) (∃' p✝)
Tactic:
exact (hp.accum 𝚺).dummy_pi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.strict_mono
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
this : ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
⊢ Hierarchy Γ' s' p
Tactic:
simpa [show s + (s' - s.succ) + 1 = s' from by simpa [Nat.succ_add] using Nat.add_sub_of_le h] using this (s' - s.succ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.strict_mono
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
Tactic:
intro d
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
d : ℕ
⊢ Hierarchy Γ' (s + d + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.strict_mono
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
d : ℕ
⊢ Hierarchy Γ' (s + d + 1) p
Tactic:
induction' d with s ih
Proof state after:
case zero
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ Hierarchy Γ' (s + 0 + 1) p

case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s✝ : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s✝ p
Γ' : Polarity
s' : ℕ
h : s✝ < s'
s : ℕ
ih : Hierarchy Γ' (s✝ + s + 1) p
⊢ Hierarchy Γ' (s✝ + (s + 1) + 1) p
Theorem: LO.FirstOrder.Arith.Hierarchy.strict_mono
Proof state before:
case zero
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ Hierarchy Γ' (s + 0 + 1) p
Tactic:
simpa using hp.accum Γ'
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.strict_mono
Proof state before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s✝ : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s✝ p
Γ' : Polarity
s' : ℕ
h : s✝ < s'
s : ℕ
ih : Hierarchy Γ' (s✝ + s + 1) p
⊢ Hierarchy Γ' (s✝ + (s + 1) + 1) p
Tactic:
simpa only [Nat.add_succ, add_zero] using ih.accum _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.strict_mono
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
this : ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
⊢ s + (s' - s.succ) + 1 = s'
Tactic:
simpa [Nat.succ_add] using Nat.add_sub_of_le h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.mono
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
⊢ Hierarchy Γ s' p
Tactic:
rcases Nat.lt_or_eq_of_le h with (lt | rfl)
Proof state after:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
lt : s < s'
⊢ Hierarchy Γ s' p

case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s
⊢ Hierarchy Γ s p
Theorem: LO.FirstOrder.Arith.Hierarchy.mono
Proof state before:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
lt : s < s'
⊢ Hierarchy Γ s' p
Tactic:
exact hp.strict_mono Γ lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.mono
Proof state before:
case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s
⊢ Hierarchy Γ s p
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.of_zero
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' s p
Tactic:
rcases Nat.eq_or_lt_of_le (Nat.zero_le s) with (rfl | pos)
Proof state after:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' 0 p

case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
pos : 0 < s
⊢ Hierarchy b' s p
Theorem: LO.FirstOrder.Arith.Hierarchy.of_zero
Proof state before:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' 0 p
Tactic:
exact zero_iff.mp hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.of_zero
Proof state before:
case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
pos : 0 < s
⊢ Hierarchy b' s p
Tactic:
exact strict_mono hp b' pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.equal
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]
Proof state after:
no goals