update & Exp

Arithmetization/Basic/IOpen.lean

@@ -7,13 +7,13 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 
 section IOpen
 
-variable [𝐈open.Mod M]
+variable [M ⊧ₘ* 𝐈open]
 
 @[elab_as_elim]
 lemma open_induction {P : M → Prop}
@@ -626,16 +626,16 @@ end IOpen
 
 section polynomial_induction
 
-variable [𝐈open.Mod M]
+variable [M ⊧ₘ* 𝐈open]
 variable {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
 @[elab_as_elim]
-lemma hierarchy_polynomial_induction (Γ ν) [(Theory.indScheme L (Arith.Hierarchy Γ ν)).Mod M]
-    {P : M → Prop} (hP : DefinablePred L Γ ν P)
+lemma hierarchy_polynomial_induction (Γ n) [M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ n)]
+    {P : M → Prop} (hP : DefinablePred L Γ n P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x := by
   intro x; induction x using order_induction_h
   · exact Γ
-  · exact ν
+  · exact n
   · exact hP
   case inst => exact inferInstance
   case inst => exact inferInstance
@@ -649,15 +649,15 @@ lemma hierarchy_polynomial_induction (Γ ν) [(Theory.indScheme L (Arith.Hierarc
 
 end polynomial_induction
 
-@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₀ [𝐈𝚺₀.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
+@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₀ [M ⊧ₘ* 𝐈𝚺₀] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x :=
   hierarchy_polynomial_induction Σ 0 hP zero even odd
 
-@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₁ [𝐈𝚺₁.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
+@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₁ [M ⊧ₘ* 𝐈𝚺₁] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x :=
   hierarchy_polynomial_induction Σ 1 hP zero even odd
 
-@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_pi₁ [𝐈𝚷₁.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Π 1 P)
+@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_pi₁ [M ⊧ₘ* 𝐈𝚷₁] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Π 1 P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x :=
   hierarchy_polynomial_induction Π 1 hP zero even odd
 

Arithmetization/Basic/Ind.lean

@@ -2,8 +2,6 @@ import Arithmetization.Basic.PeanoMinus
 
 namespace LO.FirstOrder
 
-attribute [simp] Theory.Mod.modelsTheory
-
 namespace Arith
 
 namespace Theory
@@ -40,18 +38,18 @@ variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
 
 section
 
-variable [𝐏𝐀⁻.Mod M] {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
+variable [M ⊧ₘ* 𝐏𝐀⁻] {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
 section IndScheme
 
-variable {C : Semiformula L ℕ 1 → Prop} [(Theory.indScheme L C).Mod M]
+variable {C : Semiformula L ℕ 1 → Prop} [M ⊧ₘ* Theory.indScheme L C]
 
 private lemma induction_eval {p : Semiformula L ℕ 1} (hp : C p) (v) :
     Semiformula.Eval! M ![0] v p →
     (∀ x, Semiformula.Eval! M ![x] v p → Semiformula.Eval! M ![x + 1] v p) →
     ∀ x, Semiformula.Eval! M ![x] v p := by
   have : M ⊧ₘ (∀ᶠ* succInd p) :=
-    Theory.Mod.models (T := Theory.indScheme _ C) M (by simpa using Theory.mem_indScheme_of_mem hp)
+    ModelsTheory.models (T := Theory.indScheme _ C) M (by simpa using Theory.mem_indScheme_of_mem hp)
   simp [models_iff, succInd, Semiformula.eval_substs,
     Semiformula.eval_rew_q Rew.toS, Function.comp, Matrix.constant_eq_singleton] at this
   exact this v
@@ -68,7 +66,7 @@ end IndScheme
 
 section neg
 
-variable (Γ : Polarity) (s : ℕ) [(Theory.indScheme L (Arith.Hierarchy Γ s)).Mod M]
+variable (Γ : Polarity) (s : ℕ) [M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ s)]
 
 @[elab_as_elim]
 lemma induction_h {P : M → Prop} (hP : DefinablePred L Γ s P)
@@ -142,7 +140,7 @@ lemma models_indScheme_alt : M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ.al
           by intro x; simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]⟩
   exact this H0 Hsucc x
 
-instance : (Theory.indScheme L (Arith.Hierarchy Γ.alt s)).Mod M := ⟨models_indScheme_alt Γ s⟩
+instance : M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ.alt s) := models_indScheme_alt Γ s
 
 lemma least_number_h {P : M → Prop} (hP : DefinablePred L Γ s P)
     {x} (h : P x) : ∃ y, P y ∧ ∀ z < y, ¬P z := by
@@ -169,59 +167,59 @@ lemma least_number_h {P : M → Prop} (hP : DefinablePred L Γ s P)
 
 end neg
 
-instance [(Theory.indScheme L (Arith.Hierarchy Σ s)).Mod M] :
-    (Theory.indScheme L (Arith.Hierarchy Γ s)).Mod M := by
+instance [M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Σ s)] :
+    M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ s) := by
   rcases Γ
   · exact inferInstance
-  · exact ⟨models_indScheme_alt Σ s⟩
+  · exact models_indScheme_alt Σ s
 
 end
 
-def mod_iOpen_of_mod_indH (Γ s) [(𝐈𝐍𝐃Γ s).Mod M] : 𝐈open.Mod M :=
-  Theory.Mod.of_ss (T₁ := 𝐈𝐍𝐃Γ s) M (Set.union_subset_union_right _ (Theory.indScheme_subset Hierarchy.of_open))
+def mod_iOpen_of_mod_indH (Γ n) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] : M ⊧ₘ* 𝐈open :=
+  ModelsTheory.of_ss (U := 𝐈𝐍𝐃Γ n) inferInstance
+    (Set.union_subset_union_right _ (Theory.indScheme_subset Hierarchy.of_open))
 
-def mod_iSigma_of_le {s₁ s₂} (h : s₁ ≤ s₂) [(𝐈𝚺 s₂).Mod M] : (𝐈𝚺 s₁).Mod M :=
-  Theory.Mod.of_ss M (Theory.iSigma_subset_mono h)
+def mod_iSigma_of_le {n₁ n₂} (h : n₁ ≤ n₂) [M ⊧ₘ* 𝐈𝚺 n₂] : M ⊧ₘ* 𝐈𝚺 n₁ :=
+  ModelsTheory.of_ss inferInstance (Theory.iSigma_subset_mono h)
 
-instance [𝐈open.Mod M] : 𝐏𝐀⁻.Mod M := Theory.Mod.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
+instance [M ⊧ₘ* 𝐈open] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
 
-instance [𝐈𝚺₀.Mod M] : 𝐈open.Mod M := mod_iOpen_of_mod_indH Σ 0
+instance [M ⊧ₘ* 𝐈𝚺₀] : M ⊧ₘ* 𝐈open := mod_iOpen_of_mod_indH Σ 0
 
-instance [𝐈𝚺₁.Mod M] : 𝐈𝚺₀.Mod M := mod_iSigma_of_le (show 0 ≤ 1 from by simp)
+instance [M ⊧ₘ* 𝐈𝚺₁] : M ⊧ₘ* 𝐈𝚺₀ := mod_iSigma_of_le (show 0 ≤ 1 from by simp)
 
-instance [(𝐈𝚺 ν).Mod M] : (𝐈𝐍𝐃 Γ ν).Mod M := by
-  rcases Γ
-  · exact inferInstance
-  · haveI : 𝐏𝐀⁻.Mod M := Arith.mod_peanoMinus_of_mod_indH (Γ := Σ) (ν := ν)
-    exact inferInstance
+instance [M ⊧ₘ* 𝐈𝚺 n] : M ⊧ₘ* 𝐈𝚷 n :=
+  haveI : M ⊧ₘ* 𝐏𝐀⁻ := Arith.models_peanoMinus_of_models_indH Σ n
+  inferInstance
+
+instance [M ⊧ₘ* 𝐈𝚷 n] : M ⊧ₘ* 𝐈𝚺 n :=
+  haveI : M ⊧ₘ* 𝐏𝐀⁻ := Arith.models_peanoMinus_of_models_indH Π n
+  by simp [*]; simpa [Theory.iPi] using models_indScheme_alt (L := ℒₒᵣ) (M := M) Π n
 
-instance [(𝐈𝚷 ν).Mod M] : (𝐈𝚺 ν).Mod M :=
-  haveI : 𝐏𝐀⁻.Mod M := Arith.mod_peanoMinus_of_mod_indH (Γ := Π) (ν := ν)
-  Theory.Mod.of_models (by simpa [Theory.iPi] using models_indScheme_alt (M := M) Π ν)
+lemma models_iSigma_iff_models_iPi {n} : M ⊧ₘ* 𝐈𝚺 n ↔ M ⊧ₘ* 𝐈𝚷 n :=
+  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
 
-lemma models_iSigma_iff_models_iPi : M ⊧ₘ* 𝐈𝚺 ν ↔ M ⊧ₘ* 𝐈𝚷 ν :=
-  ⟨fun h ↦ by haveI : (𝐈𝚺 ν).Mod M := ⟨h⟩; exact Theory.Mod.modelsTheory M _,
-   fun h ↦ by haveI : (𝐈𝚷 ν).Mod M := ⟨h⟩; exact Theory.Mod.modelsTheory M _⟩
+instance [M ⊧ₘ* 𝐈𝚺 n] : M ⊧ₘ* 𝐈𝐍𝐃Γ n := by rcases Γ <;> exact inferInstance
 
-@[elab_as_elim] lemma induction_iSigmaZero [𝐈𝚺₀.Mod M]
+@[elab_as_elim] lemma induction_iSigmaZero [M ⊧ₘ* 𝐈𝚺₀]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x := induction_h Σ 0 hP zero succ
 
-@[elab_as_elim] lemma induction_iSigmaOne [𝐈𝚺₁.Mod M]
+@[elab_as_elim] lemma induction_iSigmaOne [M ⊧ₘ* 𝐈𝚺₁]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x := induction_h Σ 1 hP zero succ
 
-@[elab_as_elim] lemma order_induction_iSigmaZero [𝐈𝚺₀.Mod M]
+@[elab_as_elim] lemma order_induction_iSigmaZero [M ⊧ₘ* 𝐈𝚺₀]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x :=
   order_induction_h Σ 0 hP ind
 
-@[elab_as_elim] lemma order_induction_iSigmaOne [𝐈𝚺₁.Mod M]
+@[elab_as_elim] lemma order_induction_iSigmaOne [M ⊧ₘ* 𝐈𝚺₁]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x :=
   order_induction_h Σ 1 hP ind
 
-lemma least_number_iSigmaZero [𝐈𝚺₀.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
+lemma least_number_iSigmaZero [M ⊧ₘ* 𝐈𝚺₀] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     {x} (h : P x) : ∃ y, P y ∧ ∀ z < y, ¬P z :=
   least_number_h Σ 0 hP h
 

Arithmetization/Basic/PeanoMinus.lean

@@ -6,7 +6,7 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 

Arithmetization/Definability/Definability.lean

@@ -34,7 +34,7 @@ namespace Arith
 
 section definability
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 variable {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
 namespace Definability

Arithmetization/IDeltaZero/Basic.lean

@@ -9,13 +9,13 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Nonempty M] [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Nonempty M] [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚺₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₀]
 
 
 end ISigma₀

Arithmetization/IDeltaZero/Exponential/Exp.lean

@@ -12,7 +12,7 @@ namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 def ext (u z : M) : M := z / u % u
 
@@ -87,7 +87,8 @@ def Exp.Seqₛ.def : Δ₀-Sentence 3 := ⟨
       ∃[#0 < #4 + 1] (!extDef [#0, #1, #4] ∧ !extDef [2 * (#0 * #0), #1 * #1, #4])))”, by simp⟩
 
 lemma Exp.Seqₛ.defined : Δ₀-Relation₃ (Exp.Seqₛ : M → M → M → Prop) via Exp.Seqₛ.def := by
-  intro v; simp [Exp.Seqₛ.iff, Exp.Seqₛ.def, ppow2_defined.pval, ext_defined.pval, ←le_iff_lt_succ, sq]
+  intro v; simp [Exp.Seqₛ.iff, Exp.Seqₛ.def, ppow2_defined.pval,
+    ext_defined.pval, ←le_iff_lt_succ, sq, numeral_eq_natCast]
 
 lemma Exp.graph_iff (x y : M) :
     Exp x y ↔
@@ -110,7 +111,8 @@ def Exp.def : Δ₀-Sentence 2 := ⟨
       ∃[#0 < #4 * #4 + 1] (#0 ≠ 2 ∧ !ppow2Def [#0] ∧ !extDef [#3, #0, #2] ∧!extDef [#4, #0, #1])))”, by simp⟩
 
 lemma Exp.defined : Δ₀-Relation (Exp : M → M → Prop) via Exp.def := by
-  intro v; simp [Exp.graph_iff, Exp.def, ppow2_defined.pval, ext_defined.pval, Exp.Seqₛ.defined.pval, ←le_iff_lt_succ, pow_four, sq]
+  intro v; simp [Exp.graph_iff, Exp.def, ppow2_defined.pval, ext_defined.pval,
+    Exp.Seqₛ.defined.pval, ←le_iff_lt_succ, pow_four, sq, numeral_eq_natCast]
 
 instance exp_definable : DefinableRel ℒₒᵣ Σ 0 (Exp : M → M → Prop) := defined_to_with_param _ Exp.defined
 
@@ -682,7 +684,7 @@ end ISigma₀
 
 section ISigma₁
 
-variable [𝐈𝚺₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₁]
 
 namespace Exp
 
@@ -700,9 +702,7 @@ lemma range_exists_unique (x : M) : ∃! y, Exp x y := by
 
 end Exp
 
-def exponential (a : M) : M := Classical.choose! (Exp.range_exists_unique a)
-
-prefix:80 "exp " => exponential
+instance : _root_.Exp M := ⟨fun a ↦ Classical.choose! (Exp.range_exists_unique a)⟩
 
 section exponential
 
@@ -714,15 +714,15 @@ def expdef : Δ₀-Sentence 2 := ⟨“!Exp.def [#1, #0]”, by simp⟩
 
 -- #eval expdef.val
 
-lemma exp_defined : Δ₀-Function₁ (exponential : M → M) via expdef := by
+lemma exp_defined : Δ₀-Function₁ (Exp.exp : M → M) via expdef := by
   intro v; simp [expdef, exponential_graph, Exp.defined.pval]
 
-instance exponential_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (exponential : M → M) := defined_to_with_param _ exp_defined
+instance exponential_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (Exp.exp : M → M) := defined_to_with_param _ exp_defined
 
 lemma exponential_of_exp {a b : M} (h : Exp a b) : exp a = b :=
   Eq.symm <| exponential_graph.mpr h
 
-lemma exponential_inj : Function.Injective (exponential : M → M) := λ a _ H ↦
+lemma exponential_inj : Function.Injective (Exp.exp : M → M) := λ a _ H ↦
   (exp_exponential a).inj (exponential_graph.mp H)
 
 @[simp] lemma exp_zero : exp (0 : M) = 1 := exponential_of_exp (by simp)

Arithmetization/IDeltaZero/Exponential/Log.lean

@@ -12,7 +12,7 @@ namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 lemma log_exists_unique_pos {y : M} (hy : 0 < y) : ∃! x, x < y ∧ ∃ y' ≤ y, Exp x y' ∧ y < 2 * y' := by
   have : ∃ x < y, ∃ y' ≤ y, Exp x y' ∧ y < 2 * y' := by
@@ -70,7 +70,7 @@ lemma log_graph {x y : M} : x = log y ↔ (y = 0 → x = 0) ∧ (0 < y → x < y
 def logDef : Δ₀-Sentence 2 := ⟨“(#1 = 0 → #0 = 0) ∧ (0 < #1 → #0 < #1 ∧ ∃[#0 < #2 + 1] (!Exp.def [#1, #0] ∧ #2 < 2 * #0))”, by simp⟩
 
 lemma log_defined : Δ₀-Function₁ (log : M → M) via logDef := by
-  intro v; simp [logDef, log_graph, Exp.defined.pval, ←le_iff_lt_succ]
+  intro v; simp [logDef, log_graph, Exp.defined.pval, ←le_iff_lt_succ, numeral_eq_natCast]
 
 instance log_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (log : M → M) := defined_to_with_param _ log_defined
 
@@ -408,7 +408,7 @@ lemma fbit_eq_zero_of_le {a i : M} (hi : ‖a‖ ≤ i) : fbit a i = 0 := by sim
 def fbitDef : Δ₀-Sentence 3 := ⟨“∃[#0 < #2 + 1] (!bexpDef [#0, #2, #3] ∧ ∃[#0 < #3 + 1] (!divDef [#0, #3, #1] ∧ !remDef [#2, #0, 2]))”, by simp⟩
 
 lemma fbit_defined : Δ₀-Function₂ (fbit : M → M → M) via fbitDef := by
-  intro v; simp [fbitDef, bexp_defined.pval, div_defined.pval, rem_defined.pval, ←le_iff_lt_succ, fbit]
+  intro v; simp [fbitDef, bexp_defined.pval, div_defined.pval, rem_defined.pval, ←le_iff_lt_succ, fbit, numeral_eq_natCast]
   constructor
   · intro h; exact ⟨bexp (v 1) (v 2), by simp, rfl, _, by simp, rfl, h⟩
   · rintro ⟨_, _, rfl, _, _, rfl, h⟩; exact h
@@ -437,7 +437,7 @@ end ISigma₀
 
 section ISigma₁
 
-variable [𝐈𝚺₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₁]
 
 @[simp] lemma log_exponential (a : M) : log (exp a) = a := (exp_exponential a).log_eq_of_exp
 

Arithmetization/IDeltaZero/Exponential/PPow2.lean

@@ -12,7 +12,7 @@ namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 def SPPow2 (m : M) : Prop := ¬LenBit 1 m ∧ LenBit 2 m ∧ ∀ i ≤ m, Pow2 i → 2 < i → (LenBit i m ↔ (√i)^2 = i ∧ LenBit (√i) m)
 
@@ -23,7 +23,8 @@ def sppow2Def : Δ₀-Sentence 1 :=
 
 lemma sppow2_defined : Δ₀-Predicate (SPPow2 : M → Prop) via sppow2Def := by
   intro v
-  simp [SPPow2, sppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval, pow2_defined.pval, sqrt_defined.pval, ←le_iff_lt_succ, sq]
+  simp [SPPow2, sppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval,
+    pow2_defined.pval, sqrt_defined.pval, ←le_iff_lt_succ, sq, numeral_eq_natCast]
   intro _ _; apply ball_congr; intro x _; apply imp_congr_right; intro _; apply imp_congr_right; intro _; apply iff_congr
   · simp
   · constructor
@@ -36,7 +37,8 @@ def ppow2Def : Δ₀-Sentence 1 :=
   ⟨“!pow2Def [#0] ∧ ∃[#0 < 2 * #1] (!sppow2Def [#0] ∧ !lenbitDef [#1, #0])”, by simp⟩
 
 lemma ppow2_defined : Δ₀-Predicate (PPow2 : M → Prop) via ppow2Def := by
-  intro v; simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval, pow2_defined.pval, sppow2_defined.pval]
+  intro v; simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail,
+    lenbit_defined.pval, pow2_defined.pval, sppow2_defined.pval, numeral_eq_natCast]
 
 instance ppow2_definable : DefinablePred ℒₒᵣ Σ 0 (PPow2 : M → Prop) := defined_to_with_param₀ _ ppow2_defined
 

Arithmetization/IDeltaZero/Exponential/Pow2.lean

@@ -12,7 +12,7 @@ namespace Model
 
 section IOpen
 
-variable [𝐈open.Mod M]
+variable [M ⊧ₘ* 𝐈open]
 
 def Pow2 (a : M) : Prop := 0 < a ∧ ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
 
@@ -22,7 +22,7 @@ def pow2Def : Δ₀-Sentence 1 :=
 lemma pow2_defined : Δ₀-Predicate (Pow2 : M → Prop) via pow2Def := by
   intro v
   simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton,
-    Pow2, pow2Def, le_iff_lt_succ, dvd_defined.pval]
+    Pow2, pow2Def, le_iff_lt_succ, dvd_defined.pval, numeral_eq_natCast]
 
 instance pow2_definable : DefinablePred ℒₒᵣ Σ 0 (Pow2 : M → Prop) := defined_to_with_param _ pow2_defined
 
@@ -114,7 +114,8 @@ def lenbitDef : Δ₀-Sentence 2 :=
   ⟨“∃[#0 < #2 + 1] (!divDef [#0, #2, #1] ∧ ¬!dvdDef [2, #0])”, by simp⟩
 
 lemma lenbit_defined : Δ₀-Relation (LenBit : M → M → Prop) via lenbitDef := by
-  intro v; simp[sqrt_graph, lenbitDef, Matrix.vecHead, Matrix.vecTail, div_defined.pval, dvd_defined.pval, LenBit, ←le_iff_lt_succ]
+  intro v; simp[sqrt_graph, lenbitDef, Matrix.vecHead, Matrix.vecTail,
+    div_defined.pval, dvd_defined.pval, LenBit, ←le_iff_lt_succ, numeral_eq_natCast]
   constructor
   · intro h; exact ⟨v 1 / v 0, by simp, rfl, h⟩
   · rintro ⟨z, hz, rfl, h⟩; exact h
@@ -193,7 +194,7 @@ end IOpen
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 namespace Pow2