Version of exact? giving all matching results

Stream: mathlib4

[Sébastien Gouëzel]

Often, I find that exact? is able to close the goal, but by applying a lemma which is obviously not the right one (e.g., taking advantages of weird defeqs, or using one direction of an iff lemma while the direction exists as a standalone lemma, or suggesting rfl when there is a lemma saying exactly what I need, that I could use in a sequence of rewrites for instance). MWE:

def foo {α : Type} (x : α) : α := x
theorem foo_def {α : Type} (x : α) : foo x = x := rfl
theorem foo_def2 {α : Type} (x : α) : foo x = x := by exact?

The exact? suggests rfl, while a suggestion to use foo_def would clearly be better.

Would it be easy to have a variant exact!? or exact?? that gives all the working results, instead of only the first one, to let the user pick whichever is best?

[Kim Morrison]

Yes, this should be easy, and I would merge a PR that does this. I would suggest exact?* as the syntax perhaps? Not sure there.

[Filippo A. E. Nuccio]

I like exact?! as "a stronger version of exact?"

[Ruben Van de Velde]

Not a general solution, but often rw? finds something better

[Patrick Massot]

This wouldn’t really be stronger, I think exact?* is better.

[Kim Morrison]

Exactly --- I don't like the ! because we're not asking it to try any harder, just to not stop at the first successful result. I suspect it really is a small change to implement, and you wouldn't need to go into the internals at all.

[Eric Wieser]

Would a with_reducible exact? be possible, for this specific case?

[Kyle Miller]

How about exact?? ?

[Kyle Miller]

Oh, sorry, Sébastien already suggested that :-)

[Vincent Beffara]

How about exact‽ ?

[Kim Morrison]

I will happily merge a PR implementing either exact?* or exact?? (hint hint :-)

[Calle Sönne]

Has anyone made this? Otherwise I can give this a go

[Calle Sönne]

Okay I have a working prototype of this. Should this be PRd to mathlib, batteries or lean core?

A related question is: can I reuse private definitions in other files? I needed to adjust some functions in
Lean/Meta/Tactic/LibrarySearch.lean. However these rely on private definitions in that file, so if I want to PR this to mathlib do I have to manually copy over all the private definitions that I need to use? Or can I somehow reuse them?

[Kevin Buzzard]

Demo it at LLL today!

[Calle Sönne]

I could! Although this was quite simple to make as exact? pretty much had all the functionality already, I just had to choose to store it :)