grind: cannot run `cases` on type that is a class field

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When a type is defined class field, there is no way to ask grind to run its case module on the type

Context

In Mathlib's category theory, Quiver.Hom instances are often (but not always) structures on which it would make sense to run cases when proving things about them. While grind [MyStruct] works fine, as soon as MyStruct appears "aliased" via a class field (such as Quiver.Hom), it is no longer possible to destruct them without making all Quiver.Hom reducible.

Steps to Reproduce

/--
info: Lean 4.31.0-nightly-2026-05-21
Target: x86_64-unknown-linux-gnu
-/
#guard_msgs in
#version
class Quiver (V : Type) where
  Hom : V → V → Type

infixr:10 " ⟶ " => Quiver.Hom

opaque S : Type

namespace Test1

structure MyHom where
  x : Nat
  hx : x = 0

example (h h' : MyHom) :
  h = h' := by grind [MyHom]

instance : Quiver S where
  Hom _ _ := MyHom

attribute [grind] Quiver.Hom
/--
error: `grind` failed
case grind
x y : S
h h' : x ⟶ y
h_1 : ¬h = h'
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] ¬h = h'
    [prop] Quiver.Hom = Quiver.Hom
  [eqc] False propositions
    [prop] h = h'
  [ematch] E-matching patterns
    [thm] Quiver.Hom.eq_1: [@Quiver.Hom #1 #0]
[grind] Diagnostics
  [thm] E-Matching instances
    [thm] Quiver.Hom.eq_1 ↦ 1
-/
#guard_msgs in
example {x y : S} (h h' : x ⟶ y) :
    h = h' := by 
  grind [MyHom]

Expected behavior: the grind call successfully destructs x ⟶ y as a Hom, or there is a way to achieve that without additional lemmas and without marking Quiver.Hom reducible.

Actual behavior: the grind call fails. In this particular example, marking Quiver.Hom as reducible fixes this, but one may not want to mark all Quiver.Hom reducible (e.g., in Mathlib).

Versions

info: Lean 4.31.0-nightly-2026-05-21
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal Lean reproducer in the issue and inspect how grind handles case modules for types reached through class fields. Done means the final grind example succeeds without making Quiver.Hom reducible, additional lemmas, or other changes beyond the reported behavior.