`grind` failing to apply lemma if instance is not syntactically equal

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

In this code:

structure A where

class B (α : Type u) where
  data : Bool

instance instB {α : Type u} : B α where
  data := false

@[grind =]
theorem data_eq : B.data A = false := rfl

class C (α : Type u) extends B α where

instance instCA : C A where

example : instCA.toB = instB := by
  with_reducible_and_instances rfl

theorem foo : B.data A = false := by grind -- `grind` failed

I expect that grind is able to apply the theorem data_eq. The type of data_eq is

theorem data_eq : @Eq Bool (@B.data A (@instB A)) false

whereas the type of foo is

theorem foo : @Eq Bool (@B.data A (@C.toB A instCA)) false

but the two instances are equal at instances transparency, so I expect the lemma to still apply.

Context

This kind of instances-defeq diamond appears everywhere. I hit it in relation to our order API.

Steps to Reproduce

1. See above code

Expected behavior: grind successfully proves foo.

Actual behavior: grind does not prove foo.

Versions

Lean 4.35.0-nightly-2026-09-08 on live.lean-lang.org

Impact

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

Start with the self-contained Lean example in the issue and reproduce the failure of grind on theorem foo using the reported nightly environment. Investigate how grind matches the [grind =] theorem data_eq when its instances are only equal at instances transparency; done means the example proves foo successfully and the regression is covered.