Theorem: LO.FirstOrder.Semiformula.eval_bexClosure (Arithmetization/Vorspiel/Vorspiel.lean)

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
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

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]
State after:
no goals

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]
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

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
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

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⟩
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

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⟩
State after:
no goals

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⟩
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

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
State after:
no goals