RFC: make deprecations generate a `try this:` suggestion when possible

Proposal

Deprecations of lemmas, definitions, options and named arguments generate a try this: suggestion when there is a direct replacement. (This applies to e.g. mere option names or argument names, and also in most cases where a declaration is just renamed.)

When the types of the deprecated and replacement declaration differ, it's fine (for now) to not generate a suggestion. Generating a suggestion for this case would also be nice, but is more involved in general. The above case should absolutely not wait on a general solution!

• User Experience: How does this feature improve the user experience?

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?
  Users can automate dealing with most warnings from breaking changes, hence spend their time on more useful aspects. This simplifies dealing with breaking changes for any Lean project. Breaking changes are still common; automating as much of this as possible is a clear win.
  This will particular benefit projects depending on mathlib, as mathlib still undergoes rapid breaking changes.

• Maintainability: Will this change streamline code maintenance or simplify its structure?
  This will be a great boon to dealing with breaking changes. I expect this to also help with deprecations in Lean core (but this is my guess).

• Context in mathlib

Community Feedback

• Deprecations from renaming lemmas are by far the most common change in mathlib. Thanks to the deprecation system, these don't break downstream projects upgrading any more --- but their warnings must be applied manually. This is tedious and silly, especially since this change can mostly be automated. Burning AI credits on this is stupid when there's is a more robust solution available.

• This is blocking resolving a big pile of mathlib tech debt around misnamed lemmas.
  Mathlib has a huge number of lemmas that are misnamed (e.g., simps projections foo_coe instead of coe_foo, Zulip ). Fixing these is impossible without proper automatic tooling.
  The difficult parts of this are already in place: a Lean-based declarations diff can detect declarations which need deprecations, we have scripts to generate these, skimmer can apply try this: suggestions automatically. The missing piece of the puzzle is Lean generating try this: suggestions for deprecations.

• This has been discussed over and over on the mathlib Zulip. Let me know if you prefer actual links here.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading Lean's deprecation system and the existing declaration-diff tooling described in the issue. Compare how skimmer applies try this: suggestions with how deprecation warnings are generated. Done means direct replacements for deprecated lemmas, definitions, options, and named arguments produce suggestions when their types match, while differing types may remain unsupported.