internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
case zero
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin 0 → Semiformula L ξ 1
q : Semiformula L ξ 0
⊢ (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin 0 → M), (∀ (i : Fin 0), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
Tactic:
simp [Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (Evalf s ε) (ballClosure p q) ↔
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
Tactic:
simp [ball_closure_succ, IH]
Proof state after:
case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∀ (e : Fin n → M),
      (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q) ↔
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∀ (e : Fin n → M),
      (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q) ↔
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
Tactic:
constructor
Proof state after:
case succ.mp
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∀ (e : Fin n → M),
      (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q) →
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q

case succ.mpr
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q) →
    ∀ (e : Fin n → M),
      (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
case succ.mp
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∀ (e : Fin n → M),
      (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q) →
    ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
Tactic:
intro H e h
Proof state after:
case succ.mp
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
H :
  ∀ (e : Fin n → M),
    (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q
e : Fin (n + 1) → M
h : ∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)
⊢ (Eval s e ε) q
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
case succ.mpr
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q) →
    ∀ (e : Fin n → M),
      (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) → ∀ (x : M), (Eval s ![x] ε) (p 0) → (Eval s (x :> e) ε) q
Tactic:
intro H e h x hx
Proof state after:
case succ.mpr
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
H : ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
e : Fin n → M
h : ∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)
x : M
hx : (Eval s ![x] ε) (p 0)
⊢ (Eval s (x :> e) ε) q
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
case succ.mpr
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
H : ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
e : Fin n → M
h : ∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)
x : M
hx : (Eval s ![x] ε) (p 0)
⊢ (Eval s (x :> e) ε) q
Tactic:
exact H (x :> e) (Fin.cases (by simpa [Matrix.empty_eq] using hx) (fun i ↦ by simpa using h i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
H : ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
e : Fin n → M
h : ∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)
x : M
hx : (Eval s ![x] ε) (p 0)
⊢ (Eval s ![(x :> e) 0] ε) (p 0)
Tactic:
simpa [Matrix.empty_eq] using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballClosure
Proof state before:
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (ballClosure p q) ↔ ∀ (e : Fin n → M), (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
H : ∀ (e : Fin (n + 1) → M), (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) → (Eval s e ε) q
e : Fin n → M
h : ∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)
x : M
hx : (Eval s ![x] ε) (p 0)
i : Fin n
⊢ (Eval s ![(x :> e) i.succ] ε) (p i.succ)
Tactic:
simpa using h i
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin n → Semiformula L ξ 1
q : Semiformula L ξ n
⊢ (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Tactic:
induction' n with n IH
Proof state after:
case zero
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin 0 → Semiformula L ξ 1
q : Semiformula L ξ 0
⊢ (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin 0), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q

case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
case zero
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
p : Fin 0 → Semiformula L ξ 1
q : Semiformula L ξ 0
⊢ (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin 0), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Tactic:
simp [Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Tactic:
simp [bex_closure_succ, IH]
Proof state after:
case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q) ↔
    ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
case succ
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q) ↔
    ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Tactic:
constructor
Proof state after:
case succ.mp
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q) →
    ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q

case succ.mpr
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q) →
    ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
case succ.mp
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q) →
    ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Tactic:
rintro ⟨e, he, x, hx, H⟩
Proof state after:
case succ.mp.intro.intro.intro.intro
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
e : Fin n → M
he : ∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)
x : M
hx : (Eval s ![x] ε) (p 0)
H : (Eval s (x :> e) ε) q
⊢ ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
case succ.mp.intro.intro.intro.intro
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
e : Fin n → M
he : ∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)
x : M
hx : (Eval s ![x] ε) (p 0)
H : (Eval s (x :> e) ε) q
⊢ ∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
Tactic:
exact ⟨x :> e, Fin.cases hx he, H⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
case succ.mpr
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
⊢ (∃ e, (∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q) →
    ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q
Tactic:
rintro ⟨e, h, H⟩
Proof state after:
case succ.mpr.intro.intro
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
e : Fin (n + 1) → M
h : ∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)
H : (Eval s e ε) q
⊢ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i.succ)) ∧ ∃ x, (Eval s ![x] ε) (p 0) ∧ (Eval s (x :> e) ε) q
Theorem: LO.FirstOrder.Semiformula.eval_bexClosure
Proof state before:
ξ : Type u_2
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n✝ : ℕ
ε : ξ → M
n : ℕ
IH :
  ∀ {p : Fin n → Semiformula L ξ 1} {q : Semiformula L ξ n},
    (Evalf s ε) (bexClosure p q) ↔ ∃ e, (∀ (i : Fin n), (Eval s ![e i] ε) (p i)) ∧ (Eval s e ε) q
p : Fin (n + 1) → Semiformula L ξ 1
q : Semiformula L ξ (n + 1)
e : Fin (n + 1) → M
h : ∀ (i : Fin (n + 1)), (Eval s ![e i] ε) (p i)
H : (Eval s e ε) q
⊢ (Eval s (e 0 :> fun x => e x.succ) ε) q
Tactic:
simpa [Matrix.eq_vecCons'] using H
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_operator₃
Proof state before:
ξ : Type u_3
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
e : Fin n → M
o : Operator L 3
t₁ t₂ t₃ : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t₁, t₂, t₃]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂, Semiterm.val s e ε t₃]
Tactic:
simp [eval_operator]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_operator₄
Proof state before:
ξ : Type u_3
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
e : Fin n → M
o : Operator L 4
t₁ t₂ t₃ t₄ : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t₁, t₂, t₃, t₄]) ↔
    o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂, Semiterm.val s e ε t₃, Semiterm.val s e ε t₄]
Tactic:
simp [eval_operator]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ballClosure_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
p : Semiformula L ξ n
v : Fin n → Semiterm L ξ 1
hv : ∀ (i : Fin n), (v i).Positive
⊢ Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p
Tactic:
induction' n with n IH <;> simp [ballClosure, ←Rew.comp_app]
Proof state after:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ Hierarchy b s (ballClosure (fun x => “#0 < !!(v x.succ)”) (“(∀[#0 < !!([→ #0] (v 0))] !p)”)) ↔ Hierarchy b s p
Theorem: LO.FirstOrder.Arith.Hierarchy.ballClosure_iff
Proof state before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ Hierarchy b s (“(∀[#0 < !!([→ #0] (v 0))] !p)”) ↔ Hierarchy b s p
Tactic:
rw [ball_iff]
Proof state after:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ([→ #0] (v 0)).Positive
Theorem: LO.FirstOrder.Arith.Hierarchy.ballClosure_iff
Proof state before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ([→ #0] (v 0)).Positive
Tactic:
simp [Semiterm.bv_eq_empty_of_positive (hv 0)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.ballClosure_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ∀ (i : Fin n), ((fun x => v x.succ) i).Positive
Tactic:
intro
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
i✝ : Fin n
⊢ ((fun x => v x.succ) i✝).Positive
Theorem: LO.FirstOrder.Arith.Hierarchy.ballClosure_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
i✝ : Fin n
⊢ ((fun x => v x.succ) i✝).Positive
Tactic:
simp [hv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bexClosure_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
p : Semiformula L ξ n
v : Fin n → Semiterm L ξ 1
hv : ∀ (i : Fin n), (v i).Positive
⊢ Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p
Tactic:
induction' n with n IH <;> simp [bexClosure, ←Rew.comp_app]
Proof state after:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ Hierarchy b s (bexClosure (fun x => “#0 < !!(v x.succ)”) (“(∃[#0 < !!([→ #0] (v 0))] !p)”)) ↔ Hierarchy b s p
Theorem: LO.FirstOrder.Arith.Hierarchy.bexClosure_iff
Proof state before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ Hierarchy b s (“(∃[#0 < !!([→ #0] (v 0))] !p)”) ↔ Hierarchy b s p
Tactic:
rw [bex_iff]
Proof state after:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ([→ #0] (v 0)).Positive
Theorem: LO.FirstOrder.Arith.Hierarchy.bexClosure_iff
Proof state before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ([→ #0] (v 0)).Positive
Tactic:
simp [Semiterm.bv_eq_empty_of_positive (hv 0)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Hierarchy.bexClosure_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ∀ (i : Fin n), ((fun x => v x.succ) i).Positive
Tactic:
intro
Proof state after:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
i✝ : Fin n
⊢ ((fun x => v x.succ) i✝).Positive
Theorem: LO.FirstOrder.Arith.Hierarchy.bexClosure_iff
Proof state before:
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
i✝ : Fin n
⊢ ((fun x => v x.succ) i✝).Positive
Tactic:
simp [hv]
Proof state after:
no goals