`grind` reaches maximum recursion depth on relatively simple goal

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

Here is some code:

module

namespace Char

def flipCase (c : Char) : Char :=
  if c.isLower then
    c.toUpper
  else if c.isUpper then
    c.toLower
  else
    c

@[simp]
theorem toNat_mk' {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
  simp [← toNat_val]

theorem isLower_flipCase {c : Char} : c.flipCase.isLower ↔ c.isUpper := by
  -- This proof works
  grind [flipCase, isUpper, isLower, toUpper, toLower]

theorem toLower_flipCase {c : Char} : c.flipCase.toLower = c.toLower := by
  -- This proof does not work. It fails with `maximum recursion depth has been reached`
  -- grind [flipCase, isUpper, isLower, toUpper, toLower]

  -- This proof works
  simp [flipCase, isUpper, isLower, toUpper, toLower, ← toNat_inj, apply_dite Char.toNat,
    apply_ite Char.toNat, UInt32.le_iff_toNat_le]
  grind

end Char

Context

Discovered during human-eval-lean.

Steps to Reproduce

1. Copy the above code into live.lean-lang.org

Expected behavior: grind [flipCase, isUpper, isLower, toUpper, toLower] solves the theorem toLower_flipCase.

Actual behavior: maximum recursion depth has been reached

Versions

4.30.0-nightly-2026-03-24 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 by running the self-contained Char example in live.lean-lang.org and reproduce the failure in toLower_flipCase with grind [flipCase, isUpper, isLower, toUpper, toLower]. Compare it with the working isLower_flipCase proof and the expanded workaround; done means the direct grind invocation solves the theorem without reaching maximum recursion depth.