From 30ecacd6250ee3f15e7729ad4dd56b515b2ad72d Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 27 Oct 2025 15:18:55 +1100
Subject: [PATCH] feat: add LawfulOfScientific class (#10971)

This PR adds a `LawfulOfScientific` class, providing compatibility with
a `Lean.Grind.Field` structure.
---
 src/Init/Grind/Ring.lean              |  1 +
 src/Init/Grind/Ring/OfScientific.lean | 29 +++++++++++++++++++++++++++
 src/Init/GrindInstances/Ring/Rat.lean |  5 ++++-
 3 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 src/Init/Grind/Ring/OfScientific.lean

diff --git a/src/Init/Grind/Ring.lean b/src/Init/Grind/Ring.lean
index ecaf400a6b..2f5d344f76 100644
--- a/src/Init/Grind/Ring.lean
+++ b/src/Init/Grind/Ring.lean
@@ -7,6 +7,7 @@ module
 prelude
 public import Init.Grind.Ring.Basic
 public import Init.Grind.Ring.Field
+public import Init.Grind.Ring.OfScientific
 public import Init.Grind.Ring.Envelope
 public import Init.Grind.Ring.CommSolver
 public import Init.Grind.Ring.CommSemiringAdapter
diff --git a/src/Init/Grind/Ring/OfScientific.lean b/src/Init/Grind/Ring/OfScientific.lean
new file mode 100644
index 0000000000..d569787905
--- /dev/null
+++ b/src/Init/Grind/Ring/OfScientific.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Init.Grind.Ring.Field
+public import Init.Data.OfScientific
+
+public section
+
+namespace Lean.Grind
+
+attribute [local instance] Semiring.natCast
+
+/--
+A type class that ensures that `OfScientific.ofScientific` is properly defined with respect to
+the field structure.
+-/
+class LawfulOfScientific (α : Type u) [Field α] [OfScientific α] : Prop where
+  /--
+  `OfScientific.ofScientific` is properly defined with respect to the field structure.
+  -/
+  ofScientific_def :
+    OfScientific.ofScientific m s e = if s then (Nat.cast m : α) / 10^e else (Nat.cast m : α) * 10^e
+
+end Lean.Grind
diff --git a/src/Init/GrindInstances/Ring/Rat.lean b/src/Init/GrindInstances/Ring/Rat.lean
index 5971415892..e2916f5a81 100644
--- a/src/Init/GrindInstances/Ring/Rat.lean
+++ b/src/Init/GrindInstances/Ring/Rat.lean
@@ -6,7 +6,7 @@ Authors: Robin Arnez
 module
 
 prelude
-public import Init.Grind.Ring.Field
+public import Init.Grind.Ring.OfScientific
 public import Init.Data.Rat.Lemmas
 
 public section
@@ -56,4 +56,7 @@ instance : NoNatZeroDivisors Rat where
     change k * a = k * b at h₂
     simpa [← Rat.mul_assoc, Rat.inv_mul_cancel, h₁] using congrArg ((k : Rat)⁻¹ * ·) h₂
 
+instance : LawfulOfScientific Rat where
+  ofScientific_def {m s e} := by rw [Rat.ofScientific_def_eq_if]
+
 end Lean.Grind