internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.induction_eval
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
this : M ⊧ₘ ∀ᶠ* succInd p
⊢ (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:
simp [models_iff, succInd, Semiformula.eval_substs,
  Semiformula.eval_rew_q Rew.toS, Function.comp, Matrix.constant_eq_singleton] at this
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
this :
  ∀ (ε : ℕ → 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
⊢ (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
Theorem: LO.FirstOrder.Arith.Model.induction_eval
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
this :
  ∀ (ε : ℕ → 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
⊢ (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:
exact this v
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.induction_eval
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
⊢ ∀ᶠ* succInd p ∈ Theory.indScheme L C
Tactic:
simpa using Theory.mem_indScheme_of_mem hp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.induction
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
P : M → Prop
hP : ∃ e p, C p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x
Tactic:
rcases hP with ⟨e, p, Cp, hp⟩
Proof state after:
case intro.intro.intro
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
P : M → Prop
e : ℕ → M
p : Semiformula L ℕ 1
Cp : C p
hp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x
Theorem: LO.FirstOrder.Arith.Model.induction
Proof state before:
case intro.intro.intro
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
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
P : M → Prop
e : ℕ → M
p : Semiformula L ℕ 1
Cp : C p
hp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x
Tactic:
simpa [←hp] using induction_eval (M := M) Cp e
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
rcases hP with ⟨p, hp⟩
Proof state after:
case mk.intro
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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Theorem: LO.FirstOrder.Arith.Model.induction_h
Proof state before:
case mk.intro
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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
haveI : Inhabited M := Classical.inhabited_of_nonempty'
Proof state after:
case mk.intro
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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Theorem: LO.FirstOrder.Arith.Model.induction_h
Proof state before:
case mk.intro
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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ ∃ e p, Hierarchy Γ m p ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
Tactic:
exact ⟨p.val.fvEnumInv, (Rew.rewriteMap p.val.fvEnum).hom p.val, by simp [hp],
  by  intro x; simp [Semiformula.eval_rewriteMap]
      have : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val :=
        Semiformula.eval_iff_of_funEqOn _ (by intro x hx; simp [Semiformula.fvEnumInv_fvEnum hx])
      simp [this, hp.df.iff]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ Hierarchy Γ m ((Rew.rewriteMap p.val.fvEnum).hom p.val)
Tactic:
simp [hp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
⊢ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] p.val.fvEnumInv) ((Rew.rewriteMap p.val.fvEnum).hom p.val)
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 : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.val.fvEnumInv) ((Rew.rewriteMap p.val.fvEnum).hom p.val)
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.val.fvEnumInv) ((Rew.rewriteMap p.val.fvEnum).hom p.val)
Tactic:
simp [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 : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val
Tactic:
have : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val :=
  Semiformula.eval_iff_of_funEqOn _ (by intro x hx; simp [Semiformula.fvEnumInv_fvEnum hx])
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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this✝ : Inhabited M
x : M
this : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this✝ : Inhabited M
x : M
this : (Semiformula.Evalm M ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm M ![x] id) p.val
⊢ P x ↔ (Semiformula.Eval inst✝³ ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val
Tactic:
simp [this, hp.df.iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ Function.funEqOn p.val.fvar? (fun x => p.val.fvEnumInv (p.val.fvEnum x)) id
Tactic:
intro x hx
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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x✝ x : M
hx : p.val.fvar? x
⊢ (fun x => p.val.fvEnumInv (p.val.fvEnum x)) x = id x
Theorem: LO.FirstOrder.Arith.Model.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
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x✝ x : M
hx : p.val.fvar? x
⊢ (fun x => p.val.fvEnumInv (p.val.fvEnum x)) x = id x
Tactic:
simp [Semiformula.fvEnumInv_fvEnum hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
⊢ ∀ (x : M), P x
Tactic:
suffices ∀ x, ∀ y < x, P y by
  intro x; exact this (x + 1) x (by simp only [lt_add_iff_pos_right, lt_one_iff_eq_zero])
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
ind : ∀ (x : M), (∀ y < x, P y) → P x
⊢ ∀ (x y : M), y < x → P y
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
⊢ ∀ (x y : M), y < x → P y
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ ∀ y < x, P y
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
⊢ ∀ y < 0, P y
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ Structure.ORing L M
Tactic:
case inst => exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
Tactic:
case inst => exact inferInstance
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
this : ∀ (x y : M), y < x → P y
⊢ ∀ (x : M), P x
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 : M → Prop
hP : DefinablePred L (Γ.coe, m) P
ind : ∀ (x : M), (∀ y < x, P y) → P x
this : ∀ (x y : M), y < x → P y
x : M
⊢ P x
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
this : ∀ (x y : M), y < x → P y
x : M
⊢ P x
Tactic:
exact this (x + 1) x (by simp only [lt_add_iff_pos_right, lt_one_iff_eq_zero])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
this : ∀ (x y : M), y < x → P y
x : M
⊢ x < x + 1
Tactic:
simp only [lt_add_iff_pos_right, lt_one_iff_eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_induction_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
⊢ Polarity
Tactic:
exact Γ
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_induction_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
⊢ ℕ
Tactic:
exact m
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_induction_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ DefinablePred ?m.128738 (Γ.coe, m) fun x => ∀ y < x, P y
Tactic:
suffices DefinablePred L (Γ, m) fun x => ∀ y < x, P y 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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ DefinablePred L (Γ.coe, m) fun x => ∀ y < x, P y
Theorem: LO.FirstOrder.Arith.Model.order_induction_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ DefinablePred L (Γ.coe, m) fun x => ∀ y < x, P y
Tactic:
exact Definable.ball_lt₀ (L := L) (by simp) (hP.retraction ![0])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
this : DefinablePred L (Γ.coe, m) fun x => ∀ y < x, P y
⊢ DefinablePred ?m.128738 (Γ.coe, m) fun x => ∀ y < x, P y
Tactic:
exact this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.order_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
ind : ∀ (x : M), (∀ y < x, P y) → P x
x : M
⊢ DefinableBoundedFunction L (Γ.coe, m) fun v => v 0
Tactic:
simp
Proof state after:
no goals