simp? returns unuseful lemmas

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

/--
info: Try this:
  [apply] simp only [ge_iff_le]
-/
#guard_msgs (substring := true) in
example {x : Rat} : 0 ≤ x := by
  have : 0 ≤ x := by sorry
  simp?

The above code gives ge_iff_le as one of the simp lemmas, despite this lemma not being useful or needed in the call.

Context

This is another instance of a regression in simp from Lean 3.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.3F.20giving.20nonsense.20lemmas

Steps to Reproduce

1. Code as above.

Expected behavior: simp? returns the lemmas needed in a simp only call.

Actual behavior: simp? returns nonsense lemmas.

Versions

Version: Lean 4.31.0-nightly-2026-04-30
OS version: live.lean-lang.org.

Additional Information

This is the same issue as #4534, but while the fix there resolved that example, this one remains.

Impact

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

Start with the minimal reproducer in the issue and run the simp? entry point against the stated Lean nightly version. Trace how the suggested simp only lemmas are selected for the 0 ≤ x example. Done means the suggestion no longer includes the unnecessary ge_iff_le lemma and still reports the lemmas needed to reproduce the result.