Theorem: LO.FirstOrder.Arith.Hierarchy.bexClosure_iff (Arithmetization/Vorspiel/Vorspiel.lean)

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

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

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

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

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