exact? fails to close goal

[TwoFX]

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

The exact? tactic fails to solve the following goal:

class LinearO (α : Type) (le : α → α → Prop) : Prop where
class IsTri (α : Type) (le : α → α → Prop) : Prop where

instance [LinearO α le] : IsTri α le where

def IsAnti (le : α → α → Prop) (s : α) : Prop := sorry
def IsSubsingleton (s : α) : Prop := sorry

theorem IsAnti.isSubsingleton [IsTri α le] {s : α} (h : IsAnti le s) : IsSubsingleton s := sorry

example [LinearO α le] {s : α} (h : IsAnti le s) : IsSubsingleton s := by
  exact? -- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

Context

Minimized from this Zulip message

Steps to Reproduce

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

Expected behavior: exact? finds the proof exact IsAnti.isSubsingleton h.

Actual behavior: exact? cannot close the goal. apply? finds the lemma but fails to find the matching hypothesis. exact? using h and apply? using h both do not find anything. When changing LinearO to IsTri in the example, exact? succeeds.

Versions

4.16.0-nightly-2025-01-15 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.