internlm/Lean-Github huggingface dataset:
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚷, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
⊢ DefinedWithParam (fun v => ∃ x < f v, P v x)
    (HSemiformula.mkPi (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.val)))”) ⋯)
Tactic:
intro v
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚷, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
v : Fin k → M
⊢ (fun v => ∃ x < f v, P v x) v ↔
    (Semiformula.Evalm M v id)
      (HSemiformula.mkPi (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.val)))”) ⋯).val
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚷, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
v : Fin k → M
⊢ (fun v => ∃ x < f v, P v x) v ↔
    (Semiformula.Evalm M v id)
      (HSemiformula.mkPi (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.val)))”) ⋯).val
Tactic:
simp [hbf.df.iff, hp.df.iff]
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
⊢ Hierarchy 𝚺 (m + 1) (“∃' (!bf.val ∧ (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.sigma.val)))”)
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
⊢ DefinedWithParam (fun v => ∃ x < f v, P v x)
    (HSemiformula.mkSigma (“∃' (!bf.val ∧ (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.sigma.val)))”)
      ⋯)
Tactic:
intro v
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
v : Fin k → M
⊢ (fun v => ∃ x < f v, P v x) v ↔
    (Semiformula.Evalm M v id)
      (HSemiformula.mkSigma
          (“∃' (!bf.val ∧ (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.sigma.val)))”) ⋯).val
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
v : Fin k → M
⊢ (fun v => ∃ x < f v, P v x) v ↔
    (Semiformula.Evalm M v id)
      (HSemiformula.mkSigma
          (“∃' (!bf.val ∧ (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.sigma.val)))”) ⋯).val
Tactic:
simp [hbf.df.iff, hp.df.iff, HSemiformula.val_sigma]
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
⊢ Hierarchy 𝚷 (m + 1) (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.pi.val)))”)
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
⊢ DefinedWithParam (fun v => ∃ x < f v, P v x)
    (HSemiformula.mkPi (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.pi.val)))”) ⋯)
Tactic:
intro v
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
v : Fin k → M
⊢ (fun v => ∃ x < f v, P v x) v ↔
    (Semiformula.Evalm M v id)
      (HSemiformula.mkPi (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.pi.val)))”)
          ⋯).val
Theorem: Arith.Model.Definable.bex_lt
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
bf : HSemiformula L M (k + 1) (𝚺, m + 1)
hbf : DefinedWithParam (fun v => v 0 = f fun x => v x.succ) bf
p : HSemiformula L M k.succ (𝚫, m + 1)
hp : DefinedWithParam (fun w => P (fun x => w x.succ) (w 0)) p
v : Fin k → M
⊢ (fun v => ∃ x < f v, P v x) v ↔
    (Semiformula.Evalm M v id)
      (HSemiformula.mkPi (“∀' (!bf.val → (∃[#0 < #1] !((Rew.substs (#0 :> fun x => #x.succ.succ)).hom p.pi.val)))”)
          ⋯).val
Tactic:
simp [hbf.df.iff, hp.df.iff, hp.proper.iff']
Proof state after:
no goals
Theorem: Arith.Model.Definable.ball_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable L (Γ, m + 1) fun v => ∀ x ≤ f v, P v x
Tactic:
have : Definable L (Γ, m + 1) (fun v ↦ ∀ x < f v + 1, P v x) := ball_lt (DefinableFunction₂.comp (by simp) hf (by simp)) h
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∀ x < f v + 1, P v x
⊢ Definable L (Γ, m + 1) fun v => ∀ x ≤ f v, P v x
Theorem: Arith.Model.Definable.ball_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∀ x < f v + 1, P v x
⊢ Definable L (Γ, m + 1) fun v => ∀ x ≤ f v, P v x
Tactic:
exact this.of_iff <| by intro v; simp [lt_succ_iff_le]
Proof state after:
no goals
Theorem: Arith.Model.Definable.ball_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction₂ L (𝚺, m + 1) HAdd.hAdd
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.ball_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction L (𝚺, m + 1) fun v => 1
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.ball_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∀ x < f v + 1, P v x
⊢ ∀ (x : Fin k → M), (∀ x_1 ≤ f x, P x x_1) ↔ ∀ x_1 < f x + 1, P x x_1
Tactic:
intro v
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∀ x < f v + 1, P v x
v : Fin k → M
⊢ (∀ x ≤ f v, P v x) ↔ ∀ x < f v + 1, P v x
Theorem: Arith.Model.Definable.ball_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∀ x < f v + 1, P v x
v : Fin k → M
⊢ (∀ x ≤ f v, P v x) ↔ ∀ x < f v + 1, P v x
Tactic:
simp [lt_succ_iff_le]
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable L (Γ, m + 1) fun v => ∃ x ≤ f v, P v x
Tactic:
have : Definable L (Γ, m + 1) (fun v ↦ ∃ x < f v + 1, P v x) := bex_lt (DefinableFunction₂.comp (by simp) hf (by simp)) h
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∃ x < f v + 1, P v x
⊢ Definable L (Γ, m + 1) fun v => ∃ x ≤ f v, P v x
Theorem: Arith.Model.Definable.bex_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∃ x < f v + 1, P v x
⊢ Definable L (Γ, m + 1) fun v => ∃ x ≤ f v, P v x
Tactic:
exact this.of_iff <| by intro v; simp [lt_succ_iff_le]
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction₂ L (𝚺, m + 1) HAdd.hAdd
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction L (𝚺, m + 1) fun v => 1
Tactic:
simp
Proof state after:
no goals
Theorem: Arith.Model.Definable.bex_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∃ x < f v + 1, P v x
⊢ ∀ (x : Fin k → M), (∃ x_1 ≤ f x, P x x_1) ↔ ∃ x_1 < f x + 1, P x x_1
Tactic:
intro v
Proof state after:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∃ x < f v + 1, P v x
v : Fin k → M
⊢ (∃ x ≤ f v, P v x) ↔ ∃ x < f v + 1, P v x
Theorem: Arith.Model.Definable.bex_le
Proof state before:
L : Language
inst✝⁹ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : M ⊧ₘ* 𝐏𝐀⁻
inst✝² : Structure L M
inst✝¹ : Structure.ORing L M
inst✝ : Structure.Monotone L M
Γ✝ : HierarchySymbol
k : ℕ
P✝ Q : (Fin k → M) → Prop
m : ℕ
Γ : SigmaPiDelta
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction L (𝚺, m + 1) f
h : Definable L (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable L (Γ, m + 1) fun v => ∃ x < f v + 1, P v x
v : Fin k → M
⊢ (∃ x ≤ f v, P v x) ↔ ∃ x < f v + 1, P v x
Tactic:
simp [lt_succ_iff_le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
this : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
⊢ ∃! x, x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Tactic:
rcases this with ⟨x, hx⟩
Proof state after:
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
x : M
hx : x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
⊢ ∃! x, x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
hy : 0 < y
⊢ ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Tactic:
induction y using hierarchy_polynomial_induction_oRing_sigma₀
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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'

case even
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝¹ : x✝ > 0
a✝ : 0 < x✝ → ∃ x < x✝, ∃ y' ≤ x✝, Exponential x y' ∧ x✝ < 2 * y'
hy : 0 < 2 * x✝
⊢ ∃ x < 2 * x✝, ∃ y' ≤ 2 * x✝, Exponential x y' ∧ 2 * x✝ < 2 * y'

case odd
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x✝ : M
a✝ : 0 < x✝ → ∃ x < x✝, ∃ y' ≤ x✝, Exponential x y' ∧ x✝ < 2 * y'
hy : 0 < 2 * x✝ + 1
⊢ ∃ x < 2 * x✝ + 1, ∃ y' ≤ 2 * x✝ + 1, Exponential x y' ∧ 2 * x✝ + 1 < 2 * y'
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
Tactic:
case zero => simp at hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'
Tactic:
case even y _ IH =>
  rcases (IH (by simpa using hy) : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
  exact ⟨x + 1, lt_of_lt_of_le (by simp [hxy]) (succ_le_double_of_pos (pos_of_gt hxy)),
    2 * y', by simpa using gey, Exponential.exponential_succ_mul_two.mpr H, by simpa using lty⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
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 ⊧ₘ* 𝐈𝚫₀
⊢ 𝚺₀-Predicate fun {y} => 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
hy : 0 < 0
⊢ ∃ x < 0, ∃ y' ≤ 0, Exponential x y' ∧ 0 < 2 * y'
Tactic:
simp at hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.log_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'
Tactic:
rcases (IH (by simpa using hy) : ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y') with ⟨x, hxy, y', gey, H, lty⟩
Proof state after:
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y : M
a✝ : y > 0
IH : 0 < y → ∃ x < y, ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
hy : 0 < 2 * y
x : M
hxy : x < y
y' : M
gey : y' ≤ y
H : Exponential x y'
lty : y < 2 * y'
⊢ ∃ x < 2 * y, ∃ y' ≤ 2 * y, Exponential x y' ∧ 2 * y < 2 * y'