`apply?` generates references to daggered assumptions

Description

Sometimes, the library search tactics will generate references to inaccessible assumptions and include daggers in their suggestions. Accepting the suggestion leads to a broken proof.

Context

I've simply noticed this when working with Lean.

Steps to Reproduce

Enter the following proof:

example (n k : Nat) : n + k = k + n := by
  induction n <;> cases k
  . simp
  . simp
  . simp
  . apply?

Prior to apply?, the proof state is:

case succ.succ
n✝¹ n✝ : Nat
a✝ : n✝¹ + (n✝ + 1) = n✝ + 1 + n✝¹
⊢ n✝¹ + 1 + (n✝ + 1) = n✝ + 1 + (n✝¹ + 1)

Try it here

Expected behavior:

I would expect either that the suggestion included code to make the assumption accessible, or that it did not offer to insert suggestions that use inaccessible assumptions.

For instance, it could suggest:

rename_i n n' _
exact Nat.add_comm (n + 1) (n' + 1)

as the edit, or provide a message like:

Found suggestion
  exact Nat.add_comm (n✝ + 1) (n✝¹ + 1)
that relies on inaccessible assumptions n✝ and n✝¹. Please name these assumptions (e.g. with 'rename_i') to use the suggestion.

Actual behavior:
The suggestion generates code that does not parse: exact Nat.add_comm (n✝ + 1) (n✝¹ + 1):

example (n k : Nat) : n + k = k + n := by
  induction n <;> cases k
  . simp
  . simp
  . simp
  . exact Nat.add_comm (n✝ + 1) (n✝¹ + 1)

The errors are:

lean-nightly.lean:6:25

expected token

lean-nightly.lean:6:24

unknown identifier 'n'

Versions

"4.12.0-nightly-2024-09-19"

Additional Information

None

Impact

I consider this a papercut, but the library search features are so nice that polishing them seems worthwhile.

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

Reproduce the supplied Lean proof and inspect how apply? builds suggestions when the proof state contains inaccessible assumptions marked with daggers. Trace the library-search suggestion entry point and its handling of local declaration names. Done means the generated suggestion either names the assumptions accessibly or refuses to offer code that cannot parse, with coverage for this reproduction.