internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.neg_induction_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this : ∀ x ≤ a, P (a - x)
⊢ P 0
Tactic:
simpa using this a (by rfl)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.neg_induction_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
this : ∀ x ≤ a, P (a - x)
⊢ a ≤ a
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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
Proof 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
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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]))
Proof 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
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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]))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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
Proof 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)
Theorem: LO.FirstOrder.Arith.Model.models_indScheme_alt
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
⊢ ∃ y, P y ∧ ∀ z < y, ¬P z
Tactic:
by_contra A
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A : ¬∃ y, P y ∧ ∀ z < y, ¬P z
⊢ False
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A : ¬∃ y, P y ∧ ∀ z < y, ¬P z
⊢ False
Tactic:
have A : ∀ z, P z → ∃ w < z, P w := by simpa using A
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ False
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
this : ∀ (z w : M), w < z → ¬P w
⊢ False
Tactic:
exact this (x + 1) x (by simp) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A : ¬∃ y, P y ∧ ∀ z < y, ¬P z
⊢ ∀ (z : M), P z → ∃ w < z, P w
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ (z w : M), w < z → ¬P w
Tactic:
intro z
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ ∀ w < z, ¬P w
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ w < 0, ¬P w
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ Structure.ORing L M
Tactic:
case inst => exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ.alt m)
Tactic:
case inst => exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
case Γ
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ Polarity
Tactic:
exact Γ.alt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
case m
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ℕ
Tactic:
exact m
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
case hP
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred ?m.414954 (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Tactic:
suffices DefinablePred L (Γ.alt, m) fun z ↦ ∀ w < z, ¬P w by exact this
Proof state after:
case hP
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred L (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof state before:
case hP
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
⊢ DefinablePred L (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
z : M
this : DefinablePred L (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
⊢ DefinablePred ?m.414954 (Γ.alt.coe, m) fun z => ∀ w < z, ¬P w
Tactic:
exact this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
⊢ ∀ w < 0, ¬P w
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
⊢ ∀ w < x + 1, ¬P w
Tactic:
intro w hx hw
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx : w < x + 1
hw : P w
⊢ False
Theorem: LO.FirstOrder.Arith.Model.least_number_h
Proof 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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx : w < x + 1
hw : P w
⊢ False
Tactic:
rcases le_iff_lt_or_eq.mp (lt_succ_iff_le.mp hx) with (hx | rfl)
Proof state after:
case inl
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x✝ : M
h : P x✝
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
x : M
IH : ∀ w < x, ¬P w
w : M
hx✝ : w < x + 1
hw : P w
hx : w < x
⊢ False

case inr
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
x : M
h : P x
A✝ : ¬∃ y, P y ∧ ∀ z < y, ¬P z
A : ∀ (z : M), P z → ∃ w < z, P w
w : M
hw : P w
IH : ∀ w_1 < w, ¬P w_1
hx : w < w + 1
⊢ False