Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt (Arithmetization/Basic/Ind.lean)

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ.alt m)
Tactic:
simp [Theory.indH, Theory.indScheme]
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
⊢ ∀ (f : Sentence L) (x : Semiformula L ℕ 1), Hierarchy Γ.alt m x → f = ∀ᶠ* succInd x → inst✝³.toStruc ⊧ f

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
⊢ ∀ (f : Sentence L) (x : Semiformula L ℕ 1), Hierarchy Γ.alt m x → f = ∀ᶠ* succInd x → inst✝³.toStruc ⊧ f
Tactic:
rintro _ p hp rfl
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
⊢ inst✝³.toStruc ⊧ ∀ᶠ* succInd p

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
⊢ inst✝³.toStruc ⊧ ∀ᶠ* succInd p
Tactic:
simp [models_iff, succInd, Semiformula.eval_rew_q,
  Semiformula.eval_substs, Function.comp, Matrix.constant_eq_singleton]
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
⊢ ∀ (ε : ℕ → M),
    (Semiformula.Eval inst✝³ ![0] ε) p →
      (∀ (x : M), (Semiformula.Eval inst✝³ ![x] ε) p → (Semiformula.Eval inst✝³ ![x + 1] ε) p) →
        ∀ (x : M), (Semiformula.Eval inst✝³ ![x] ε) p

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
⊢ ∀ (ε : ℕ → M),
    (Semiformula.Eval inst✝³ ![0] ε) p →
      (∀ (x : M), (Semiformula.Eval inst✝³ ![x] ε) p → (Semiformula.Eval inst✝³ ![x + 1] ε) p) →
        ∀ (x : M), (Semiformula.Eval inst✝³ ![x] ε) p
Tactic:
intro v H0 Hsucc x
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
⊢ (Semiformula.Eval inst✝³ ![x] v) p

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
⊢ (Semiformula.Eval inst✝³ ![x] v) p
Tactic:
have : Semiformula.Evalm M ![0] v p →
  (∀ x, Semiformula.Evalm M ![x] v p → Semiformula.Evalm M ![x + 1] v p) →
    ∀ x, Semiformula.Evalm M ![x] v p := by
  simpa using
    neg_induction_h (L := L) Γ m (P := λ x ↦ ¬Semiformula.Evalm M ![x] v p)
      (.mkPolarity (~(Rew.rewriteMap v).hom p) (by simpa using hp)
      (by intro x; simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]))
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
this :
  (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p
⊢ (Semiformula.Eval inst✝³ ![x] v) p

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
this :
  (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p
⊢ (Semiformula.Eval inst✝³ ![x] v) p
Tactic:
exact this H0 Hsucc x
State after:
no goals

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
⊢ (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p
Tactic:
simpa using
  neg_induction_h (L := L) Γ m (P := λ x ↦ ¬Semiformula.Evalm M ![x] v p)
    (.mkPolarity (~(Rew.rewriteMap v).hom p) (by simpa using hp)
    (by intro x; simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]))
State after:
no goals

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
⊢ Hierarchy Γ m (~(Rew.rewriteMap v).hom p)
Tactic:
simpa using hp
State after:
no goals

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x : M
⊢ ∀ (v_1 : Fin 1 → M),
    (fun x => ¬(Semiformula.Evalm M ![x] v) p) (v_1 0) ↔ (Semiformula.Evalm M v_1 id) (~(Rew.rewriteMap v).hom p)
Tactic:
intro x
State after:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x✝ : M
x : Fin 1 → M
⊢ (fun x => ¬(Semiformula.Evalm M ![x] v) p) (x 0) ↔ (Semiformula.Evalm M x id) (~(Rew.rewriteMap v).hom p)

State before:
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x✝ : M
x : Fin 1 → M
⊢ (fun x => ¬(Semiformula.Evalm M ![x] v) p) (x 0) ↔ (Semiformula.Evalm M x id) (~(Rew.rewriteMap v).hom p)
Tactic:
simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]
State after:
no goals