exact?/apply?/have?/rw? and deprecated lemmas

Stream: mathlib4

[Michael Stoll]

Sometimes, exact? and friends suggest the use of deprecated lemmas, which is a bit annoying, as one has to first click on the "try this" and then replace the lemma name. Can this be avoided? I.e., is it easily possible to remove deprecated lemmas from the search?

(Not sure this is a new complaint. I only found this message when searching Zulip).

[Damiano Testa]

I think that more generally getting multiple lemmas that all work would be an improvement.

[Michael Stoll]

minus the deprecated ones...

[Damiano Testa]

Or at least flagged out.

[Damiano Testa]

(I'm thinking of a situation where the undeprecated result does not close the goal at hand: in those cases, the deprecated one is better than nothing! :smile: )

[Michael Stoll]

In most cases, the deprecated one has been replaced by something else, which should be found instead.

[Ruben Van de Velde]

Yeah, but there are also cases where the deprecated version has a slightly different statement

[Thomas Murrills]

Note that Try This allows styling of suggestions; while strikethrough of a lemma might be too illegible in the suggestion list, a “warning” styling for these suggestions might be appropriate (after pushing them to the bottom of the list!)

[Kim Morrison]

PR definitely welcome!

[Kim Morrison]

Also don't forget in this family have?.

[Michael Stoll]

Changed the topic to include have?.