`exact?` suggests an extra `id`

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

exact? suggests term with id

Context

Steps to Reproduce

1. In this proof, hover over exact? to see what it suggests: example (a : Nat) (ha : a ≠ 0) : (0 < a ∨ a < 0) := by exact?

Expected behavior:

It suggests exact Nat.lt_or_gt_of_ne (Ne.symm ha)

Actual behavior:

It suggests exact Nat.lt_or_gt_of_ne (id (Ne.symm ha)) (note the extra id)

Versions

Lean 4.16.0-nightly-2025-01-19
Target: x86_64-unknown-linux-gnu

Impact

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

Start by reproducing the minimal exact? example from the issue against the listed Lean nightly version, then trace the exact? suggestion path to find where the redundant id is introduced. Done means the same proof suggests exact Nat.lt_or_gt_of_ne (Ne.symm ha) without the extra id.