Exact? fails on le_antisymm

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Data.Real.Basic

example {x y : ℝ} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by exact?

This fails (and came up in Jakob's talk at LftCM) - is this expected behaviour?

[Alex J. Best]

The explanation for this is that conclusion a = b is very generic. so exact? skips putting such things in its discrimination tree for efficiency reasons afaiu. I definitely agree that we need to find some way to improve this situation (i.e. print a nice warning in this case at the very least, or implement an "exact? but I don't care if its slow please try with very generic lemmas in the tree also" mode).

[Scott Morrison]

Maybe at this point it is fine to just put them back in. We already prioritize trying more specific lemmas first, so hopefully the "not specific at all" lemmas would automatically be tried last.

If someone wants to try this out, just find where in LibrarySearch.lean we use insertIfSpecific and just it to insert!

[Scott Morrison]

#8459