Add terms to `try?`

Stream: lean4

[Moritz R]

First of all, a huge thank you to all the people developing on grind and the try? tactic.
It's proven (ha!) to be extremely useful to me. <3

I have a suggestion:
Sometimes i know that a specific proof term i can build (typically using 1-3 local arguments) will be really useful for discharging the goal, but grind [myterm] can't quite do it, since it's missing one or two lemmas from the library that i typically don't know by name.

How about having something to the likes of try? [myterm1, myterm2], to add these terms to the lemma filter/local assumptions?

[vibecodermcswaggins]

(deleted)

[Moritz R]

please open a different topic

[Jovan Gerbscheid]

Presumably, have := myterm1; have := myterm2; try? would do this?

[Moritz R]

good idea

[Moritz R]

would be a bit nicer though, if the wished-for try? [...] would also directly inline the term when it finds a proof

[Kim Morrison]

I'm not really sure where we would start here. try? dispatches to many different subsidiary tactics (and indeed is user extensible). I can't imagine any way of systematically passing these additional terms to the tactics, beyond just calling have first.

[Jakub Nowak]

Maybe we could add editor code action for inlining have/let, so at least you could do that manually after the fact?