feat: LawfulOfScientific in grind (#11331)

This PR adds support for the `LawfulOfScientific` class in `grind`.
Examples:
```lean
open Lean Grind Std
variable [LE α] [LT α] [LawfulOrderLT α] [Field α] [OfScientific α]
         [LawfulOfScientific α] [IsLinearOrder α] [OrderedRing α]
example : (2 / 3 : α) ≤ (0.67 : α) := by  grind
example : (1.2 : α) ≤ (1.21 : α) := by grind
example : (2 / 3 : α) ≤ (67 / 100 : α) := by grind
example : (1.2345 : α) ≤ (1.2346 : α) := by grind
example : (2.3 : α) ≤ (4.5 : α) := by grind
example : (2.3 : α) ≤ (5/2 : α) := by grind
```

Author: leodemoura

src/Init/Grind/Norm.lean

@@ -8,6 +8,7 @@ prelude
 public import Init.Data.Int.Linear
 public import Init.Grind.Ring.Field
 public import Init.Data.Rat.Lemmas
+public import Init.Grind.Ring.OfScientific
 public section
 
 namespace Lean.Grind
@@ -207,7 +208,9 @@ init_grind_norm
   Ring.intCast_mul
   Ring.intCast_pow
   Ring.intCast_sub
+  -- OfScientific
+  LawfulOfScientific.ofScientific_def
   -- Rationals
-  Rat.ofScientific_def_eq_if Rat.zpow_neg
+  Rat.zpow_neg
 
 end Lean.Grind

tests/lean/run/grind_10489.lean

@@ -8,3 +8,12 @@ example : (1.2345 : Rat) ≤ (1.2346 : Rat) := by grind
 example : (1.2345 : Rat) ≤ (1.234501 : Rat) := by grind
 example : (2.3 : Rat) ≤ (4.5 : Rat) := by grind
 example : (2.3 : Rat) ≤ (5/2 : Rat) := by grind
+
+open Lean Grind Std
+variable [LE α] [LT α] [LawfulOrderLT α] [Field α] [OfScientific α] [LawfulOfScientific α] [IsLinearOrder α] [OrderedRing α]
+example : (2 / 3 : α) ≤ (0.67 : α) := by  grind
+example : (1.2 : α) ≤ (1.21 : α) := by grind
+example : (2 / 3 : α) ≤ (67 / 100 : α) := by grind
+example : (1.2345 : α) ≤ (1.2346 : α) := by grind
+example : (2.3 : α) ≤ (4.5 : α) := by grind
+example : (2.3 : α) ≤ (5/2 : α) := by grind

tests/lean/run/grind_fin.lean

@@ -600,3 +600,7 @@ theorem pred_one {n : Nat} :
 theorem val_eq_zero_iff [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0 := by grind
 
 theorem val_ne_zero_iff [NeZero n] {a : Fin n} : a.val ≠ 0 ↔ a ≠ 0 := by grind
+
+example (n : Nat) (j k : Fin n) (hk : ↑k + 1 < n) (h : j ≠ ⟨↑k + 1, hk⟩) :
+    (if (j : Nat) = ↑k + 1 then 1 else 0) = 0 := by
+  grind