Merge pull request #6 from FormalizedFormalLogic/update-4.13

chore: Update to 4.13

Arithmetization/Basic/IOpen.lean

@@ -7,7 +7,7 @@ open FirstOrder FirstOrder.Arith
 
 noncomputable section
 
-variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐏𝐀⁻]
+variable {V : Type*} [ORingStruc V]
 
 section IOpen
 
@@ -60,48 +60,6 @@ lemma div_exists_unique_pos (a : V) {b} (pos : 0 < b) : ∃! u, b * u ≤ a ∧
       _ ≤ a           := hu'.1
     exact LT.lt.false this)
 
-/-
-lemma mod (a : V) {b} (pos : 0 < b) : ∃! u, ∃ v < b, a = b * u + v := by
-  have : ∃! u, b * u ≤ a ∧ a < b * (u + 1) := by
-    have : ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
-      have : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
-        simpa using open_leastNumber (P := λ u ↦ b * u ≤ a) ⟨“&b * #0 ≤ &a”, by simp, by intro x; simp⟩
-      simp at this
-      have hx : a < b * (a + 1) := by
-        have : a + 0 < b * a + b :=
-          add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
-        simpa [mul_add] using this
-      exact this hx
-    rcases this with ⟨u, hu⟩
-    exact ExistsUnique.intro u hu (by
-      intro u' hu'
-      by_contra ne
-      wlog lt : u < u'
-      · exact this a pos u' hu' u hu (Ne.symm ne) (Ne.lt_of_le ne $ by simpa using lt)
-      have : a < a := by calc
-        a < b * (u + 1) := hu.2
-        _ ≤ b * u'      := (_root_.mul_le_mul_left pos).mpr (lt_iff_succ_le.mp lt)
-        _ ≤ a           := hu'.1
-      exact LT.lt.false this)
-  have iff : ∀ u, (∃ v < b, a = b * u + v) ↔ (b * u ≤ a ∧ a < b * (u + 1)) := by
-    intro u; constructor
-    · rintro ⟨v, hv, rfl⟩
-      simp [mul_add, hv]
-    · intro h
-      let v := a - b * u
-      have e : a = b*u + v := by simp [add_tsub_self_of_le h.1]
-      have : v < b := by
-        by_contra hyv
-        have hyv : b ≤ v := by simpa using hyv
-        have : a < a := by calc
-          a < b * (u + 1) := h.2
-          _ ≤ b * u + v   := by simpa [mul_add] using hyv
-          _ = a           := e.symm
-        exact LT.lt.false this
-      exact ⟨v, this, e⟩
-  exact (exists_unique_congr iff).mpr this
--/
-
 section div
 
 lemma div_exists_unique (a b : V) : ∃! u, (0 < b → b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0) := by
@@ -832,19 +790,21 @@ end polynomial_induction
 
 @[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₀ [V ⊧ₘ* 𝐈𝚺₀] {P : V → Prop} (hP : 𝚺₀-Predicate 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
+  hierarchy_polynomial_induction 𝚺 0 (P := P) hP zero even odd
 
 @[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₁ [V ⊧ₘ* 𝐈𝚺₁] {P : V → Prop} (hP : 𝚺₁-Predicate 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
+  hierarchy_polynomial_induction 𝚺 1 (P := P) hP zero even odd
 
 @[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_pi₁ [V ⊧ₘ* 𝐈𝚷₁] {P : V → Prop} (hP : 𝚷₁-Predicate 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
+  hierarchy_polynomial_induction 𝚷 1 (P := P) hP zero even odd
+
+variable [V ⊧ₘ* 𝐈open]
 
-lemma nat_cast_pair (n m : ℕ) : (⟪n, m⟫ : ℕ) = ⟪(n : V), (m : V)⟫ := by simp [pair]
+lemma nat_cast_pair (n m : ℕ) : (⟪n, m⟫ : ℕ) = ⟪(↑n : V), (↑m : V)⟫ := by simp [pair]
 
-lemma nat_pair_eq (m n : ℕ) : ⟪n, m⟫ = Nat.pair n m := by simp [Arith.pair, Nat.pair]; congr
+lemma nat_pair_eq (m n : ℕ) : ⟪n, m⟫ = Nat.pair n m := by simp [Arith.pair, Nat.pair]
 
 lemma pair_coe_eq_coe_pair (m n : ℕ) :  ⟪n, m⟫ = (Nat.pair n m : V) := by simp [nat_cast_pair, nat_pair_eq]
 

Arithmetization/Basic/Ind.lean

@@ -32,8 +32,6 @@ variable {V : Type*} [ORingStruc V]
 
 section
 
-variable [V ⊧ₘ* 𝐏𝐀⁻]
-
 section IndScheme
 
 variable {C : Semiformula ℒₒᵣ ℕ 1 → Prop} [V ⊧ₘ* Theory.indScheme ℒₒᵣ C]
@@ -56,11 +54,12 @@ lemma induction {P : V → Prop}
 
 end IndScheme
 
+variable [V ⊧ₘ* 𝐏𝐀⁻]
+
 section neg
 
 variable (Γ : Polarity) (m : ℕ) [V ⊧ₘ* Theory.indScheme ℒₒᵣ (Arith.Hierarchy Γ m)]
 
-@[elab_as_elim]
 lemma induction_h {P : V → Prop} (hP : Γ-[m].BoldfacePred P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x :=
   induction (P := P) (C := Hierarchy Γ m) (by
@@ -73,7 +72,6 @@ lemma induction_h {P : V → Prop} (hP : Γ-[m].BoldfacePred P)
           simp [this, hp.df.iff]⟩)
     zero succ
 
-@[elab_as_elim]
 lemma order_induction_h {P : V → Prop} (hP : Γ-[m].BoldfacePred P)
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x := by
   suffices ∀ x, ∀ y < x, P y by

Arithmetization/Definability/Boldface.lean

@@ -23,7 +23,7 @@ variable (ξ : Type*) (n : ℕ)
 
 open LO.Arith
 
-variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻]
+variable {V : Type*} [ORingStruc V]
 
 def Defined (R : (Fin k → V) → Prop) : {ℌ : HierarchySymbol} → ℌ.Semisentence k → Prop
   | 𝚺-[_], p => FirstOrder.Defined R p.val
@@ -341,7 +341,7 @@ namespace BoldfaceRel
 @[simp] instance lt : ℌ.BoldfaceRel (LT.lt : V → V → Prop) :=
   Defined.to_definable_oRing₀ (.mkSigma “#0 < #1” (by simp)) (by intro _; simp)
 
-@[simp] instance le : ℌ.BoldfaceRel (LE.le : V → V → Prop) :=
+@[simp] instance le [V ⊧ₘ* 𝐏𝐀⁻] : ℌ.BoldfaceRel (LE.le : V → V → Prop) :=
   Defined.to_definable_oRing₀ (.mkSigma “#0 ≤ #1” (by simp)) (by intro _; simp)
 
 end BoldfaceRel
@@ -846,13 +846,13 @@ lemma bex_lt {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
       ⟨ .mkPi (∀' (bf.val ➝ (∃[“#0 < #1”] Rew.substs (#0 :> (#·.succ.succ)) |>.hom p.pi.val))) (by simp),
         by intro v; simp [hbf.df.iff, hp.df.iff, hp.proper.iff'] ⟩
 
-lemma ball_le {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
+lemma ball_le [V ⊧ₘ* 𝐏𝐀⁻] {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     (hf : 𝚺-[m + 1].BoldfaceFunction f) (h : Γ-[m + 1].Boldface (fun w ↦ P (w ·.succ) (w 0))) :
     Γ-[m + 1].Boldface (fun v ↦ ∀ x ≤ f v, P v x) := by
   have : Γ-[m + 1].Boldface (fun v ↦ ∀ x < f v + 1, P v x) := ball_lt (BoldfaceFunction₂.comp (by simp) hf (by simp)) h
   exact this.of_iff <| by intro v; simp [lt_succ_iff_le]
 
-lemma bex_le {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
+lemma bex_le [V ⊧ₘ* 𝐏𝐀⁻] {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     (hf : 𝚺-[m + 1].BoldfaceFunction f) (h : Γ-[m + 1].Boldface (fun w ↦ P (w ·.succ) (w 0))) :
     Γ-[m + 1].Boldface (fun v ↦ ∃ x ≤ f v, P v x) := by
   have : Γ-[m + 1].Boldface (fun v ↦ ∃ x < f v + 1, P v x) := bex_lt (BoldfaceFunction₂.comp (by simp) hf (by simp)) h
@@ -862,7 +862,7 @@ lemma ball_lt' {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     (hf : 𝚺-[m + 1].BoldfaceFunction f) (h : Γ-[m + 1].Boldface (fun w ↦ P (w ·.succ) (w 0))) :
     Γ-[m + 1].Boldface (fun v ↦ ∀ {x}, x < f v → P v x) := ball_lt hf h
 
-lemma ball_le' {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
+lemma ball_le' [V ⊧ₘ* 𝐏𝐀⁻] {Γ} {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     (hf : 𝚺-[m + 1].BoldfaceFunction f) (h : Γ-[m + 1].Boldface (fun w ↦ P (w ·.succ) (w 0))) :
     Γ-[m + 1].Boldface (fun v ↦ ∀ {x}, x ≤ f v → P v x) := ball_le hf h
 

Arithmetization/Definability/BoundedBoldface.lean

@@ -7,7 +7,7 @@ open LO.Arith
 
 variable {ξ : Type*} {n : ℕ}
 
-variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻]
+variable {V : Type*} [ORingStruc V]
 
 variable {ℌ : HierarchySymbol} {Γ Γ' : SigmaPiDelta}
 
@@ -30,23 +30,23 @@ variable {ℌ}
 
 namespace Bounded
 
-@[simp] lemma var {k} (i : Fin k) : Bounded fun v : Fin k → V ↦ v i := ⟨#i, by intro _; simp⟩
+@[simp] lemma var [V ⊧ₘ* 𝐏𝐀⁻] {k} (i : Fin k) : Bounded fun v : Fin k → V ↦ v i := ⟨#i, by intro _; simp⟩
 
-@[simp] lemma const {k} (c : V) : Bounded (fun _ : Fin k → V ↦ c) := ⟨&c, by intro _; simp⟩
+@[simp] lemma const [V ⊧ₘ* 𝐏𝐀⁻] {k} (c : V) : Bounded (fun _ : Fin k → V ↦ c) := ⟨&c, by intro _; simp⟩
 
-@[simp] lemma term_retraction (t : Semiterm ℒₒᵣ V n) (e : Fin n → Fin k) :
+@[simp] lemma term_retraction [V ⊧ₘ* 𝐏𝐀⁻] (t : Semiterm ℒₒᵣ V n) (e : Fin n → Fin k) :
     Bounded fun v : Fin k → V ↦ Semiterm.valm V (fun x ↦ v (e x)) id t :=
   ⟨Rew.substs (fun x ↦ #(e x)) t, by intro _; simp [Semiterm.val_substs]⟩
 
-@[simp] lemma term (t : Semiterm ℒₒᵣ V k) : Bounded fun v : Fin k → V => Semiterm.valm V v id t :=
+@[simp] lemma term [V ⊧ₘ* 𝐏𝐀⁻] (t : Semiterm ℒₒᵣ V k) : Bounded fun v : Fin k → V => Semiterm.valm V v id t :=
   ⟨t, by intro _; simp⟩
 
 lemma retraction {f : (Fin k → V) → V} (hf : Bounded f) (e : Fin k → Fin n) :
     Bounded fun v ↦ f (fun i ↦ v (e i)) := by
   rcases hf with ⟨t, ht⟩
   exact ⟨Rew.substs (fun x ↦ #(e x)) t, by intro; simp [Semiterm.val_substs, ht]⟩
 
-lemma comp {k} {f : (Fin l → V) → V} {g : Fin l → (Fin k → V) → V} (hf : Bounded f) (hg : ∀ i, Bounded (g i)) :
+lemma comp [V ⊧ₘ* 𝐏𝐀⁻] {k} {f : (Fin l → V) → V} {g : Fin l → (Fin k → V) → V} (hf : Bounded f) (hg : ∀ i, Bounded (g i)) :
     Bounded (fun v ↦ f (g · v)) where
   bounded := by
     rcases hf.bounded with ⟨tf, htf⟩
@@ -57,14 +57,14 @@ lemma comp {k} {f : (Fin l → V) → V} {g : Fin l → (Fin k → V) → V} (hf
 
 end Bounded
 
-lemma Bounded₁.comp {f : V → V} {k} {g : (Fin k → V) → V} (hf : Bounded₁ f) (hg : Bounded g) :
+lemma Bounded₁.comp [V ⊧ₘ* 𝐏𝐀⁻] {f : V → V} {k} {g : (Fin k → V) → V} (hf : Bounded₁ f) (hg : Bounded g) :
     Bounded (fun v ↦ f (g v)) := Bounded.comp hf (l := 1) (fun _ ↦ hg)
 
-lemma Bounded₂.comp {f : V → V → V} {k} {g₁ g₂ : (Fin k → V) → V}
+lemma Bounded₂.comp [V ⊧ₘ* 𝐏𝐀⁻] {f : V → V → V} {k} {g₁ g₂ : (Fin k → V) → V}
     (hf : Bounded₂ f) (hg₁ : Bounded g₁) (hg₂ : Bounded g₂) :
     Bounded (fun v ↦ f (g₁ v) (g₂ v)) := Bounded.comp hf (g := ![g₁, g₂]) (fun i ↦ by cases i using Fin.cases <;> simp [*])
 
-lemma Bounded₃.comp {f : V → V → V → V} {k} {g₁ g₂ g₃ : (Fin k → V) → V}
+lemma Bounded₃.comp [V ⊧ₘ* 𝐏𝐀⁻] {f : V → V → V → V} {k} {g₁ g₂ g₃ : (Fin k → V) → V}
     (hf : Bounded₃ f) (hg₁ : Bounded g₁) (hg₂ : Bounded g₂) (hg₃ : Bounded g₃) :
     Bounded (fun v ↦ f (g₁ v) (g₂ v) (g₃ v)) := Bounded.comp hf (g := ![g₁, g₂, g₃])
       (fun i ↦ by
@@ -73,6 +73,8 @@ lemma Bounded₃.comp {f : V → V → V → V} {k} {g₁ g₂ g₃ : (Fin k →
 
 namespace Bounded₂
 
+variable [V ⊧ₘ* 𝐏𝐀⁻]
+
 instance add : Bounded₂ ((· + ·) : V → V → V) where
   bounded := ⟨‘x y. x + y’, by intro _; simp⟩
 
@@ -132,7 +134,9 @@ end BoldfaceBoundedFunction
 
 namespace HierarchySymbol.Boldface
 
-variable {P Q : (Fin k → V) → Prop}
+variable [V ⊧ₘ* 𝐏𝐀⁻]
+
+variable  {P Q : (Fin k → V) → Prop}
 
 lemma ball_blt {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     (hf : BoldfaceBoundedFunction f) (h : ℌ.Boldface fun w ↦ P (w ·.succ) (w 0)) :
@@ -243,6 +247,8 @@ lemma of_iff {f g : (Fin k → V) → V} (H : BoldfaceBoundedFunction f) (h : 
   have : f = g := by funext v; simp [h]
   rcases this; exact H
 
+variable [V ⊧ₘ* 𝐏𝐀⁻]
+
 @[simp] lemma var {k} (i : Fin k) : BoldfaceBoundedFunction (fun v : Fin k → V ↦ v i) := ⟨by simp, by simp⟩
 
 @[simp] lemma const {k} (c : V) : BoldfaceBoundedFunction (fun _ : Fin k → V ↦ c) := ⟨by simp, by simp⟩
@@ -259,6 +265,8 @@ namespace HierarchySymbol.Boldface
 
 open BoldfaceBoundedFunction
 
+variable [V ⊧ₘ* 𝐏𝐀⁻]
+
 lemma bcomp₁ {k} {P : V → Prop} {f : (Fin k → V) → V} [hP : ℌ.BoldfacePred P] (hf : BoldfaceBoundedFunction f) :
     ℌ.Boldface fun v ↦ P (f v) :=
   substitution_boldfaceBoundedFunction (f := ![f]) hP (by simp [*])
@@ -303,6 +311,8 @@ lemma bcomp₄_zero {k} {R : V → V → V → V → Prop} {f₁ f₂ f₃ f₄
 
 end HierarchySymbol.Boldface
 
+variable [V ⊧ₘ* 𝐏𝐀⁻]
+
 lemma HierarchySymbol.BoldfaceFunction.bcomp {k} {F : (Fin l → V) → V} {f : Fin l → (Fin k → V) → V}
     (hF : ℌ.BoldfaceFunction F) (hf : ∀ i, BoldfaceBoundedFunction (f i)) :
     ℌ.BoldfaceFunction (fun v ↦ F (f · v)) := by

Arithmetization/Definability/Hierarchy.lean

@@ -156,17 +156,18 @@ lemma ProperWithParamOn.iff' {p : 𝚫-[m].Semiformula M n}
 
 section ProvablyProperOn
 
-variable (T : Theory ℒₒᵣ) [𝐄𝐐 ≼ T]
+variable (T : Theory ℒₒᵣ)
 
-lemma ProvablyProperOn.ofProperOn {p : 𝚫-[m].Semisentence n}
+lemma ProvablyProperOn.ofProperOn [𝐄𝐐 ≼ T] {p : 𝚫-[m].Semisentence n}
     (h : ∀ (M : Type w) [ORingStruc M] [M ⊧ₘ* T], p.ProperOn M) : p.ProvablyProperOn T := by
   apply complete (T := T) <| FirstOrder.Arith.oRing_consequence_of.{w} T _ ?_
   intro M _ _
   simpa [models_iff] using (h M).iff
 
 variable {T}
 
-lemma ProvablyProperOn.properOn {p : 𝚫-[m].Semisentence n} (h : p.ProvablyProperOn T)
+lemma ProvablyProperOn.properOn
+    {p : 𝚫-[m].Semisentence n} (h : p.ProvablyProperOn T)
     (M : Type w) [ORingStruc M] [M ⊧ₘ* T] : p.ProperOn M := by
   intro v
   have := by simpa [models_iff] using consequence_iff.mp (sound! (T := T) h) M inferInstance

Arithmetization/ISigmaOne/Bit.lean

@@ -13,7 +13,7 @@ variable [V ⊧ₘ* 𝐈𝚺₁]
 
 def Bit (i a : V) : Prop := LenBit (exp i) a
 
-instance : Membership V V := ⟨Bit⟩
+instance : Membership V V := ⟨fun a i ↦ Bit i a⟩
 
 def _root_.LO.FirstOrder.Arith.bitDef : 𝚺₀.Semisentence 2 := .mkSigma
   “x y. ∃ z <⁺ y, !expDef z x ∧ !lenbitDef z y” (by simp)
@@ -27,9 +27,12 @@ lemma bit_defined : 𝚺₀-Relation ((· ∈ ·) : V → V → Prop) via bitDef
 @[simp] lemma bit_defined_iff (v) :
     Semiformula.Evalbm V v bitDef.val ↔ v 0 ∈ v 1 := bit_defined.df.iff v
 
-@[instance] def mem_definable : 𝚺₀-Relation ((· ∈ ·) : V → V → Prop) := bit_defined.to_definable
+instance mem_definable : 𝚺₀-Relation ((· ∈ ·) : V → V → Prop) := bit_defined.to_definable
 
-@[instance] def mem_definable' (ℌ : HierarchySymbol) : ℌ-Relation ((· ∈ ·) : V → V → Prop) := mem_definable.of_zero
+instance mem_definable' (ℌ : HierarchySymbol) : ℌ-Relation ((· ∈ ·) : V → V → Prop) := mem_definable.of_zero
+
+instance mem_definable'' (ℌ : HierarchySymbol) : ℌ-Relation (Membership.mem : V → V → Prop) := by
+  simpa using (mem_definable' ℌ).retraction (n := 2) ![1, 0]
 
 lemma mem_absolute (i a : ℕ) : i ∈ a ↔ (i : V) ∈ (a : V) := by
   simpa using Defined.shigmaZero_absolute V bit_defined bit_defined ![i, a]
@@ -48,14 +51,14 @@ section
     (hf : 𝚺-[m + 1].BoldfaceFunction f) (h : Γ-[m + 1].Boldface (fun w ↦ P (w ·.succ) (w 0))) :
     Γ-[m + 1].Boldface (fun v ↦ ∀ x ∈ f v, P v x) := by
   have : Γ-[m + 1].Boldface (fun v ↦ ∀ x < f v, x ∈ f v → P v x) :=
-    .ball_lt hf (.imp (by simpa using HierarchySymbol.Boldface.comp₂ (by simp) (hf.retraction Fin.succ)) h)
+    .ball_lt hf (.imp (HierarchySymbol.Boldface.comp₂ (P := (· ∈ ·)) (.var 0) (hf.retraction Fin.succ)) h)
   exact this.of_iff <| by intro v; exact ⟨fun h x _ hxv ↦ h x hxv, fun h x hx ↦ h x (lt_of_mem hx) hx⟩
 
 @[definability] lemma HierarchySymbol.Boldface.bex_mem (Γ m) {P : (Fin k → V) → V → Prop} {f : (Fin k → V) → V}
     (hf : 𝚺-[m + 1].BoldfaceFunction f) (h : Γ-[m + 1].Boldface (fun w ↦ P (w ·.succ) (w 0))) :
     Γ-[m + 1].Boldface (fun v ↦ ∃ x ∈ f v, P v x) := by
   have : Γ-[m + 1].Boldface (fun v ↦ ∃ x < f v, x ∈ f v ∧ P v x) :=
-    .bex_lt hf (.and (by simpa using HierarchySymbol.Boldface.comp₂ (by simp) (hf.retraction _)) h)
+    .bex_lt hf (.and (HierarchySymbol.Boldface.comp₂ (P := (· ∈ ·)) (.var 0) (hf.retraction _)) h)
   exact this.of_iff <| by
     intro v; exact ⟨by rintro ⟨x, hx, hxv⟩; exact ⟨x, lt_of_mem hx, hx, hxv⟩, by rintro ⟨x, _, hx, hvx⟩; exact ⟨x, hx, hvx⟩⟩
 
@@ -190,7 +193,7 @@ namespace LO.Arith
 
 open FirstOrder FirstOrder.Arith
 
-variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V]
+variable {V : Type*} [ORingStruc V]
 
 variable [V ⊧ₘ* 𝐈𝚺₁]
 
@@ -206,6 +209,7 @@ section empty
 
 scoped instance : EmptyCollection V := ⟨0⟩
 
+omit [V ⊧ₘ* 𝐈𝚺₁] in
 lemma emptyset_def : (∅ : V) = 0 := rfl
 
 @[simp] lemma not_mem_empty (i : V) : i ∉ (∅ : V) := by simp [emptyset_def, mem_iff_bit, Bit]
@@ -287,7 +291,7 @@ end insert
 lemma one_eq_singleton : (1 : V) = {∅} := by simp [singleton_eq_insert, insert, bitInsert, emptyset_def]
 
 @[simp] lemma mem_singleton_iff {i j : V} :
-    i ∈ ({j} : V) ↔ i = j := by simp [singleton_eq_insert]
+    i ∈ ({j} : V) ↔ i = j := by simp [singleton_eq_insert, -insert_emptyc_eq]
 
 lemma bitRemove_lt_of_mem {i a : V} (h : i ∈ a) : bitRemove i a < a := by
   simp [h, bitRemove, tsub_lt_iff_left (exp_le_of_mem h)]
@@ -482,6 +486,8 @@ section
 
 variable {m : ℕ} [Fact (1 ≤ m)] [V ⊧ₘ* 𝐈𝐍𝐃𝚺 m]
 
+omit [V ⊧ₘ* 𝐈𝚺₁]
+
 private lemma finset_comprehension_aux (Γ : Polarity) {P : V → Prop} (hP : Γ-[m]-Predicate P) (a : V) :
     haveI : V ⊧ₘ* 𝐈𝚺₁ := mod_ISigma_of_le (show 1 ≤ m from Fact.out)
     ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i := by

Arithmetization/ISigmaOne/HFS.lean

@@ -3,3 +3,4 @@ import Arithmetization.ISigmaOne.HFS.Seq
 import Arithmetization.ISigmaOne.HFS.PRF
 import Arithmetization.ISigmaOne.HFS.Fixpoint
 import Arithmetization.ISigmaOne.HFS.Vec
+import Arithmetization.ISigmaOne.HFS.Coding

Arithmetization/ISigmaOne/HFS/Basic.lean

@@ -635,7 +635,6 @@ instance sndIdx_definable' (Γ) : Γ-Function₁ (sndIdx : V → V) := sndIdx_de
 
 end sndIdx
 
-
 end LO.Arith
 
 end

Arithmetization/ISigmaOne/HFS/Coding.lean

@@ -1,11 +1,5 @@
 import Arithmetization.ISigmaOne.HFS.Vec
 
-/-!
-
-# Vec
-
--/
-
 noncomputable section
 
 namespace LO.Arith
@@ -39,7 +33,6 @@ def _root_.Finset.arithmetize (s : Finset V) : V := finsetArithmetizeAux s.toLis
     (insert a s).arithmetize = insert a s.arithmetize := mem_ext <| by
   intro x; simp
 
-
 end LO.Arith
 
 end