fix

src/Init/Grind/Ordered/Ring.lean

@@ -46,27 +46,26 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
     have := Preorder.lt_of_lt_of_le this ih
     exact Preorder.le_of_lt this
 
-instance [Ring α] [Preorder α] [Ring.IsOrdered α] : IsCharP α 0 where
-  ofNat_eq_zero_iff := by
-    intro x
-    simp only [Nat.mod_zero]; constructor
-    next =>
-      intro h
-      cases x
-      next => rfl
-      next x =>
-        rw [Semiring.ofNat_succ] at h
-        replace h := congrArg (· - 1) h; simp at h
-        rw [Ring.sub_eq_add_neg, Semiring.add_assoc, Ring.add_neg_cancel,
-            Ring.sub_eq_add_neg, Semiring.zero_add, Semiring.add_zero] at h
-        have h₁ : (OfNat.ofNat x : α) < 0 := by
-          have := Ring.IsOrdered.neg_one_lt_zero (R := α)
-          rw [h]; assumption
-        have h₂ := Ring.IsOrdered.ofNat_nonneg (R := α) x
-        have : (0 : α) < 0 := Preorder.lt_of_le_of_lt h₂ h₁
-        simp
-        exact (Preorder.lt_irrefl 0) this
-    next => intro h; rw [OfNat.ofNat, h]; rfl
+instance [Ring α] [Preorder α] [Ring.IsOrdered α] : IsCharP α 0 := IsCharP.mk' _ _ <| by
+  intro x
+  simp only [Nat.mod_zero]; constructor
+  next =>
+    intro h
+    cases x
+    next => rfl
+    next x =>
+      rw [Semiring.ofNat_succ] at h
+      replace h := congrArg (· - 1) h; simp at h
+      rw [Ring.sub_eq_add_neg, Semiring.add_assoc, Ring.add_neg_cancel,
+          Ring.sub_eq_add_neg, Semiring.zero_add, Semiring.add_zero] at h
+      have h₁ : (OfNat.ofNat x : α) < 0 := by
+        have := Ring.IsOrdered.neg_one_lt_zero (R := α)
+        rw [h]; assumption
+      have h₂ := Ring.IsOrdered.ofNat_nonneg (R := α) x
+      have : (0 : α) < 0 := Preorder.lt_of_le_of_lt h₂ h₁
+      simp
+      exact (Preorder.lt_irrefl 0) this
+  next => intro h; rw [OfNat.ofNat, h]; rfl
 
 end Preorder
 

src/Init/Grind/Ring/Basic.lean

@@ -164,6 +164,13 @@ theorem neg_eq_zero (a : α) : -a = 0 ↔ a = 0 :=
     simpa [neg_neg, neg_zero] using h,
    fun h => by rw [h, neg_zero]⟩
 
+theorem neg_eq_iff (a b : α) : -a = b ↔ a = -b := by
+  constructor
+  · intro h
+    rw [← neg_neg a, h]
+  · intro h
+    rw [← neg_neg b, h]
+
 theorem neg_add (a b : α) : -(a + b) = -a + -b := by
   rw [← add_left_inj (a + b), neg_add_cancel, add_assoc (-a), add_comm a b, ← add_assoc (-b),
     neg_add_cancel, zero_add, neg_add_cancel]
@@ -231,6 +238,14 @@ theorem intCast_add (x y : Int) : ((x + y : Int) : α) = ((x : α) + (y : α)) :
 theorem intCast_sub (x y : Int) : ((x - y : Int) : α) = ((x : α) - (y : α)) := by
   rw [Int.sub_eq_add_neg, intCast_add, intCast_neg, sub_eq_add_neg]
 
+theorem ofNat_sub {x y : Nat} (h : y ≤ x) : OfNat.ofNat (α := α) (x - y) = OfNat.ofNat x - OfNat.ofNat y := by
+  rw [ofNat_eq_natCast, ← intCast_natCast, Int.ofNat_sub h]
+  rw [intCast_sub]
+  rw [intCast_natCast, intCast_natCast, ofNat_eq_natCast, ofNat_eq_natCast]
+
+theorem neg_ofNat_sub {x y : Nat} (h : y ≤ x) : -OfNat.ofNat (α := α) (x - y) = OfNat.ofNat y - OfNat.ofNat x := by
+  rw [neg_eq_iff, ofNat_sub h, neg_sub]
+
 theorem neg_eq_neg_one_mul (a : α) : -a = (-1) * a := by
   rw [← add_left_inj a, neg_add_cancel]
   conv => rhs; arg 2; rw [← one_mul a]
@@ -300,17 +315,109 @@ end CommSemiring
 
 open Semiring Ring CommSemiring CommRing
 
-class IsCharP (α : Type u) [Ring α] (p : outParam Nat) where
-  ofNat_eq_zero_iff (p) : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0
+class IsCharP (α : Type u) [Semiring α] (p : outParam Nat) where
+  ofNat_ext_iff (p) : ∀ {x y : Nat}, OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x % p = y % p
 
 namespace IsCharP
 
-variable (p)  {α : Type u} [Ring α] [IsCharP α p]
+section
+
+variable (p) [Semiring α] [IsCharP α p]
+
+theorem ofNat_eq_zero_iff  (x : Nat) :
+    OfNat.ofNat (α := α) x = 0 ↔ x % p = 0 := by
+  rw [ofNat_ext_iff p]
+  simp
+
+theorem ofNat_ext {x y : Nat} (h : x % p = y % p) : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y := (ofNat_ext_iff p).mpr h
+
+theorem ofNat_eq_zero_iff_of_lt {x : Nat} (h : x < p) : OfNat.ofNat (α := α) x = 0 ↔ x = 0 := by
+  rw [ofNat_eq_zero_iff p, Nat.mod_eq_of_lt h]
+
+theorem ofNat_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
+    OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x = y := by
+  rw [ofNat_ext_iff p, Nat.mod_eq_of_lt h₁, Nat.mod_eq_of_lt h₂]
+
+end
+
+section Semiring
+
+variable (p)
+
+variable [Semiring α] [IsCharP α p]
 
 theorem natCast_eq_zero_iff (x : Nat) : (x : α) = 0 ↔ x % p = 0 := by
   rw [← ofNat_eq_natCast]
   exact ofNat_eq_zero_iff p x
 
+theorem natCast_ext {x y : Nat} (h : x % p = y % p) : (x : α) = (y : α) := by
+  rw [← ofNat_eq_natCast, ← ofNat_eq_natCast]
+  exact ofNat_ext p h
+
+theorem natCast_ext_iff {x y : Nat} : (x : α) = (y : α) ↔ x % p = y % p := by
+  rw [← ofNat_eq_natCast, ← ofNat_eq_natCast]
+  exact ofNat_ext_iff p
+
+theorem natCast_emod (x : Nat) : ((x % p : Nat) : α) = (x : α) := by
+  rw [natCast_ext_iff p, Nat.mod_mod]
+
+theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x := by
+  rw [ofNat_eq_natCast, ofNat_eq_natCast]
+  exact natCast_emod p x
+
+theorem natCast_eq_zero_iff_of_lt {x : Nat} (h : x < p) : (x : α) = 0 ↔ x = 0 := by
+  rw [natCast_eq_zero_iff p, Nat.mod_eq_of_lt h]
+
+theorem natCast_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
+    (x : α) = (y : α) ↔ x = y := by
+  rw [natCast_ext_iff p, Nat.mod_eq_of_lt h₁, Nat.mod_eq_of_lt h₂]
+
+end Semiring
+
+section Ring
+
+variable (p)  {α : Type u} [Ring α] [IsCharP α p]
+
+private theorem mk'_aux {x y : Nat} (p : Nat) (h : y ≤ x) :
+    (x - y) % p = 0 ↔ ∃ k₁ k₂, x + k₁ * p = y + k₂ * p := by
+  rw [Nat.mod_eq_iff]
+  by_cases h : p = 0
+  · simp [h]
+    omega
+  · have h' : 0 < p := by omega
+    simp [h, h']
+    constructor
+    · rintro ⟨k, h⟩
+      refine ⟨0, k, ?_⟩
+      simp [Nat.mul_comm]
+      omega
+    · rintro ⟨k₁, k₂, h⟩
+      have : k₁ * p ≤ k₂ * p := by omega
+      have : k₁ ≤ k₂ := Nat.le_of_mul_le_mul_right this h'
+      refine ⟨k₂ - k₁, ?_⟩
+      simp [Nat.mul_sub, Nat.mul_comm p k₁, Nat.mul_comm p k₂]
+      omega
+
+/-- Alternative constructor when `α` is a `Ring`. -/
+def mk' (p : Nat) (α : Type u) [Ring α]
+    (ofNat_eq_zero_iff : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0) : IsCharP α p where
+  ofNat_ext_iff {x y} := by
+    rw [← sub_eq_zero_iff]
+    rw [Nat.mod_eq_mod_iff]
+    by_cases h : y ≤ x
+    · have : OfNat.ofNat (α := α) x - OfNat.ofNat y = OfNat.ofNat (x - y) := by rw [ofNat_sub h]
+      rw [this, ofNat_eq_zero_iff]
+      apply mk'_aux _ h
+    · have : OfNat.ofNat (α := α) x - OfNat.ofNat (α := α) y = - OfNat.ofNat (y - x) := by rw [neg_ofNat_sub (by omega)]
+      rw [this, neg_eq_zero, ofNat_eq_zero_iff]
+      rw [mk'_aux _ (by omega)]
+      rw [exists_comm]
+      apply exists_congr
+      intro k₁
+      apply exists_congr
+      intro k₂
+      simp [eq_comm]
+
 theorem intCast_eq_zero_iff (x : Int) : (x : α) = 0 ↔ x % p = 0 :=
   match x with
   | (x : Nat) => by
@@ -346,46 +453,10 @@ theorem intCast_ext_iff {x y : Int} : (x : α) = (y : α) ↔ x % p = y % p := b
     replace this := congrArg (· + (y : α)) this
     simpa [intCast_sub, zero_add, sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero] using this
 
-theorem ofNat_ext_iff {x y : Nat} : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x % p = y % p := by
-  have := intCast_ext_iff (α := α) p (x := x) (y := y)
-  simp only [intCast_natCast, ← Int.natCast_emod] at this
-  simp only [ofNat_eq_natCast]
-  norm_cast at this
-
-theorem ofNat_ext {x y : Nat} (h : x % p = y % p) : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y := (ofNat_ext_iff p).mpr h
-
-theorem natCast_ext {x y : Nat} (h : x % p = y % p) : (x : α) = (y : α) := by
-  rw [← ofNat_eq_natCast, ← ofNat_eq_natCast]
-  exact ofNat_ext p h
-
-theorem natCast_ext_iff {x y : Nat} : (x : α) = (y : α) ↔ x % p = y % p := by
-  rw [← ofNat_eq_natCast, ← ofNat_eq_natCast]
-  exact ofNat_ext_iff p
-
 theorem intCast_emod (x : Int) : ((x % p : Int) : α) = (x : α) := by
   rw [intCast_ext_iff p, Int.emod_emod]
 
-theorem natCast_emod (x : Nat) : ((x % p : Nat) : α) = (x : α) := by
-  simp only [← intCast_natCast]
-  rw [Int.natCast_emod, intCast_emod]
-
-theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x := by
-  rw [ofNat_eq_natCast, ofNat_eq_natCast]
-  exact natCast_emod p x
-
-theorem ofNat_eq_zero_iff_of_lt {x : Nat} (h : x < p) : OfNat.ofNat (α := α) x = 0 ↔ x = 0 := by
-  rw [ofNat_eq_zero_iff p, Nat.mod_eq_of_lt h]
-
-theorem ofNat_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
-    OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y ↔ x = y := by
-  rw [ofNat_ext_iff p, Nat.mod_eq_of_lt h₁, Nat.mod_eq_of_lt h₂]
-
-theorem natCast_eq_zero_iff_of_lt {x : Nat} (h : x < p) : (x : α) = 0 ↔ x = 0 := by
-  rw [natCast_eq_zero_iff p, Nat.mod_eq_of_lt h]
-
-theorem natCast_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
-    (x : α) = (y : α) ↔ x = y := by
-  rw [natCast_ext_iff p, Nat.mod_eq_of_lt h₁, Nat.mod_eq_of_lt h₂]
+end Ring
 
 end IsCharP
 

src/Init/GrindInstances/Ring/BitVec.lean

@@ -31,8 +31,8 @@ instance : CommRing (BitVec w) where
   ofNat_succ x := BitVec.ofNat_add x 1
   intCast_neg _ := BitVec.ofInt_neg
 
-instance : IsCharP (BitVec w) (2 ^ w) where
-  ofNat_eq_zero_iff {x} := by simp [BitVec.ofInt, BitVec.toNat_eq]
+instance : IsCharP (BitVec w) (2 ^ w) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by simp [BitVec.ofInt, BitVec.toNat_eq])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add (BitVec w) (some 0) (some (2^w)) := inferInstance

src/Init/GrindInstances/Ring/Fin.lean

@@ -94,12 +94,12 @@ instance (n : Nat) [NeZero n] : CommRing (Fin n) where
   sub_eq_add_neg := Fin.sub_eq_add_neg
   intCast_neg := Fin.intCast_neg
 
-instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where
-  ofNat_eq_zero_iff x := by
+instance (n : Nat) [NeZero n] : IsCharP (Fin n) n := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     change Fin.ofNat _ _ = Fin.ofNat _ _ ↔ _
     simp only [Fin.ofNat]
     simp only [Nat.zero_mod]
-    simp only [Fin.mk.injEq]
+    simp only [Fin.mk.injEq])
 
 example [NeZero n] : ToInt.Neg (Fin n) (some 0) (some n) := inferInstance
 example [NeZero n] : ToInt.Sub (Fin n) (some 0) (some n) := inferInstance

src/Init/GrindInstances/Ring/Int.lean

@@ -29,8 +29,8 @@ instance : CommRing Int where
   ofNat_succ _ := by rfl
   sub_eq_add_neg _ _ := Int.sub_eq_add_neg
 
-instance : IsCharP Int 0 where
-  ofNat_eq_zero_iff {x} := by erw [Int.ofNat_eq_zero]; simp
+instance : IsCharP Int 0 := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by erw [Int.ofNat_eq_zero]; simp)
 
 instance : NoNatZeroDivisors Int where
   no_nat_zero_divisors k a h₁ h₂ := by

src/Init/GrindInstances/Ring/SInt.lean

@@ -39,12 +39,12 @@ instance : CommRing Int8 where
   ofNat_succ x := Int8.ofNat_add x 1
   intCast_neg := Int8.ofInt_neg
 
-instance : IsCharP Int8 (2 ^ 8) where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP Int8 (2 ^ 8) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = Int8.ofInt x := rfl
     rw [this]
     simp [Int8.ofInt_eq_iff_bmod_eq_toInt,
-      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
+      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add Int8 (some (-(2^7))) (some (2^7)) := inferInstance
@@ -75,12 +75,13 @@ instance : CommRing Int16 where
   pow_succ := Int16.pow_succ
   ofNat_succ x := Int16.ofNat_add x 1
   intCast_neg := Int16.ofInt_neg
-instance : IsCharP Int16 (2 ^ 16) where
-  ofNat_eq_zero_iff {x} := by
+
+instance : IsCharP Int16 (2 ^ 16) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = Int16.ofInt x := rfl
     rw [this]
     simp [Int16.ofInt_eq_iff_bmod_eq_toInt,
-      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
+      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add Int16 (some (-(2^15))) (some (2^15)) := inferInstance
@@ -111,12 +112,13 @@ instance : CommRing Int32 where
   pow_succ := Int32.pow_succ
   ofNat_succ x := Int32.ofNat_add x 1
   intCast_neg := Int32.ofInt_neg
-instance : IsCharP Int32 (2 ^ 32) where
-  ofNat_eq_zero_iff {x} := by
+
+instance : IsCharP Int32 (2 ^ 32) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = Int32.ofInt x := rfl
     rw [this]
     simp [Int32.ofInt_eq_iff_bmod_eq_toInt,
-      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
+      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add Int32 (some (-(2^31))) (some (2^31)) := inferInstance
@@ -147,12 +149,13 @@ instance : CommRing Int64 where
   pow_succ := Int64.pow_succ
   ofNat_succ x := Int64.ofNat_add x 1
   intCast_neg := Int64.ofInt_neg
-instance : IsCharP Int64 (2 ^ 64) where
-  ofNat_eq_zero_iff {x} := by
+
+instance : IsCharP Int64 (2 ^ 64) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = Int64.ofInt x := rfl
     rw [this]
     simp [Int64.ofInt_eq_iff_bmod_eq_toInt,
-      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
+      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add Int64 (some (-(2^63))) (some (2^63)) := inferInstance
@@ -185,12 +188,12 @@ instance : CommRing ISize where
   intCast_neg := ISize.ofInt_neg
 open System.Platform (numBits)
 
-instance : IsCharP ISize (2 ^ numBits) where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP ISize (2 ^ numBits) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = ISize.ofInt x := rfl
     rw [this]
     simp [ISize.ofInt_eq_iff_bmod_eq_toInt,
-      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right]
+      ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance

src/Init/GrindInstances/Ring/UInt.lean

@@ -145,10 +145,10 @@ instance : CommRing UInt8 where
   intCast_neg := UInt8.ofInt_neg
   intCast_ofNat := UInt8.intCast_ofNat
 
-instance : IsCharP UInt8 256 where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP UInt8 256 := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = UInt8.ofNat x := rfl
-    simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat]
+    simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add UInt8 (some 0) (some (2^8)) := inferInstance
@@ -175,10 +175,10 @@ instance : CommRing UInt16 where
   intCast_neg := UInt16.ofInt_neg
   intCast_ofNat := UInt16.intCast_ofNat
 
-instance : IsCharP UInt16 65536 where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP UInt16 65536 := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = UInt16.ofNat x := rfl
-    simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat]
+    simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add UInt16 (some 0) (some (2^16)) := inferInstance
@@ -205,10 +205,10 @@ instance : CommRing UInt32 where
   intCast_neg := UInt32.ofInt_neg
   intCast_ofNat := UInt32.intCast_ofNat
 
-instance : IsCharP UInt32 4294967296 where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP UInt32 4294967296 := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = UInt32.ofNat x := rfl
-    simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat]
+    simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add UInt32 (some 0) (some (2^32)) := inferInstance
@@ -235,10 +235,10 @@ instance : CommRing UInt64 where
   intCast_neg := UInt64.ofInt_neg
   intCast_ofNat := UInt64.intCast_ofNat
 
-instance : IsCharP UInt64 18446744073709551616 where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP UInt64 18446744073709551616 := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = UInt64.ofNat x := rfl
-    simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat]
+    simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add UInt64 (some 0) (some (2^64)) := inferInstance
@@ -267,10 +267,10 @@ instance : CommRing USize where
 
 open System.Platform
 
-instance : IsCharP USize (2 ^ numBits) where
-  ofNat_eq_zero_iff {x} := by
+instance : IsCharP USize (2 ^ numBits) := IsCharP.mk' _ _
+  (ofNat_eq_zero_iff := fun x => by
     have : OfNat.ofNat x = USize.ofNat x := rfl
-    simp [this, USize.ofNat_eq_iff_mod_eq_toNat]
+    simp [this, USize.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add USize (some 0) (some (2^numBits)) := inferInstance

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -129,7 +129,7 @@ where
     let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
     let .some commRingInst ← trySynthInstance commRing | return none
     trace_goal[grind.ring] "new ring: {type}"
-    let charInst? ← getIsCharInst? u type ringInst
+    let charInst? ← getIsCharInst? u type semiringInst
     let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let field := mkApp (mkConst ``Grind.Field [u]) type

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -160,6 +160,7 @@ where
     let hsmulFn? ← getHSMulFn?
     let hsmulNatFn? ← getHSMulNatFn?
     let ringId? ← CommRing.getRingId? type
+    let semiringInst? ← getInst? ``Grind.Semiring
     let ringInst? ← getInst? ``Grind.Ring
     let fieldInst? ← getInst? ``Grind.Field
     let getOne? : GoalM (Option Expr) := do
@@ -179,7 +180,7 @@ where
           return none
       return some inst
     let ringIsOrdInst? ← getRingIsOrdInst?
-    let charInst? ← if let some ringInst := ringInst? then getIsCharInst? u type ringInst else pure none
+    let charInst? ← if let some semiringInst := semiringInst? then getIsCharInst? u type semiringInst else pure none
     let getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
       let .some hmulInst ← trySynthInstance hmulNat | return none

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -152,9 +152,9 @@ def isIntModuleVirtualParent (parent? : Option Expr) : Bool :=
   | none => false
   | some parent => parent == getIntModuleVirtualParent
 
-def getIsCharInst? (u : Level) (type : Expr) (ringInst : Expr) : MetaM (Option (Expr × Nat)) := do withNewMCtxDepth do
+def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : MetaM (Option (Expr × Nat)) := do withNewMCtxDepth do
   let n ← mkFreshExprMVar (mkConst ``Nat)
-  let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type ringInst n
+  let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
   let .some charInst ← trySynthInstance charType | pure none
   let n ← instantiateMVars n
   let some n ← evalNat n |>.run