`apply?` returns the same suggestion many times

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

Given

example : 3 > 2 → 3 > 4 := by
  apply?

we get

Messages (140)
lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ Nat
  -- ⊢ 4 ≤ ?_
  -- ⊢ ?_ < 3

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ Nat
  -- ⊢ 4 < ?_
  -- ⊢ ?_ ≤ 3

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ 4 ≤ 2

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ 4 ≤ 3
  -- ⊢ ¬4 = 3

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ Nat
  -- ⊢ 4 < ?_
  -- ⊢ ?_ < 3

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ ¬3 ≤ 4

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ 4 < 2

lean-nightly.lean:2:2

Try this:
  [apply] refine fun a => ?_
  -- Remaining subgoals:
  -- ⊢ 3 > 2 → 3 > 4
  -- ⊢ 3 - 4 ≠ 0

and many more such suggestions. Clearly, the suggestion refine fun a => ?_ is wrong for most/all of these; the remaining subgoals don't match and it doesn't make sense for apply? to suggest refine fun a => ?_ hundreds of times.

Expected behavior: apply? returns many different suggestions.

Actual behavior: apply? returns the same suggestion many times, but with different remaining subgoals.

Versions

Lean 4.29.0-nightly-2026-01-27

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 apply? reproducer in the issue and trace the apply? suggestion-generation path. Compare the repeated suggestion text with its differing remaining subgoals; done means duplicate suggestions are eliminated and distinct valid suggestions remain without unrelated repeated messages.