feat: internalization for grind order (#10562)

This PR simplifies the `grind order` module, and internalizes the order
constraints. It removes the `Offset` type class because it introduced
too much complexity. We now cover the same use cases with a simpler
approach:
- Any type that implements at least `Std.IsPreorder`
- Arbitrary ordered rings.
- `Nat` by the `Nat.ToInt` adapter.

Author: leodemoura

src/Init/Data/Int/OfNat.lean

@@ -88,6 +88,20 @@ theorem finVal {n : Nat} {a : Fin n} {a' : Int}
     (h₁ : Lean.Grind.ToInt.toInt a = a') : NatCast.natCast (a.val) = a' := by
   rw [← h₁, Lean.Grind.ToInt.toInt, Lean.Grind.instToIntFinCoOfNatIntCast]
 
+theorem eq_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a = b) = (a' = b') := by
+  simp [← h₁, ←h₂]; constructor
+  next => intro; subst a; rfl
+  next => simp [Int.natCast_inj]
+
+theorem lt_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a < b) = (a' < b') := by
+  simp only [← h₁, ← h₂, Int.ofNat_lt]
+
+theorem le_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a ≤ b) = (a' ≤ b') := by
+  simp only [← h₁, ← h₂, Int.ofNat_le]
+
 end Nat.ToInt
 
 namespace Int.Nonneg

src/Init/Grind.lean

@@ -24,4 +24,3 @@ public import Init.Grind.Attr
 public import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.
 public import Init.Grind.AC
 public import Init.Grind.Injective
-public import Init.Grind.Order