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

This PR fixes an issue where the `Inv` instance obtained from `Field.toGrindField` was not definitionally equal to `Field.toInv` under instance reducibility. This caused `grind` to fail.

Reported at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/non.20def-eq.20.60Inv.60.20instances.20in.20.60Discriminant.2EDifferent.60

🤖 Prepared with Claude Code

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