fix(Algebra/Field): ensure Field.toGrindField.toInv is def-eq to Field.toInv

Explicitly set `inv a := a⁻¹` in `Field.toGrindField` so that `grind` can be
used in contexts where there are `InvMemClass` instances around.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: kim-em

Mathlib/Algebra/Field/Basic.lean

@@ -160,6 +160,7 @@ variable [Field K]
 
 instance (priority := 100) Field.toGrindField [Field K] : Lean.Grind.Field K :=
   { CommRing.toGrindCommRing K, ‹Field K› with
+    inv a := a⁻¹
     zpow := ⟨fun a n => a^n⟩
     zpow_zero a := by simp
     zpow_succ a n := by

MathlibTest/grind/field_instance.lean

@@ -0,0 +1,6 @@
+import Mathlib.FieldTheory.IntermediateField.Basic
+
+example {K L : Type*} [Field K] [Field L] [Algebra K L]
+    (E : IntermediateField K L) :
+    (Field.toGrindField.toInv : Inv E) = InvMemClass.inv := by
+  with_reducible_and_instances rfl