non def-eq `Inv` instances in `Discriminant.Different`

Stream: mathlib4

[Kim Morrison]

Would someone be interested in investigating an issue in Mathlib.NumberTheory.NumberField.Discriminant.Different, where there appear to be non def-eq Inv instances around?

In particular, in theorem linearDisjoint_of_isGalois_isCoprime_discr, if we change linarith [abs_discr_gt_two this]to grind [abs_discr_gt_two this] then we get the error:

error while initializing `grind ring` operators:
instance for `Inv.inv`
  InvMemClass.inv
is not definitionally equal to the expected one
  Field.toGrindField.toInv
when only reducible definitions and instances are reduced

(Perhaps @Andrew Yang, who is the author of this file? But help from anyone investigating this would be appreciated.)

[Andrew Yang]

Here is a more minimised example:

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
  delta InvMemClass.inv -- fails without this
  with_reducible_and_instances rfl

They are not equal under instance reducibility, but when I unfolded an instance it then became so.

[Kim Morrison]

Fixed in https://github.com/leanprover-community/mathlib4/pull/32711