exact? in term mode

Stream: mathlib4

[Bhavik Mehta]

Sometimes I'm trying to use exact? to find a term to close the goal (often because I can't remember its name), so I write something like

example {A : Finset ℕ} : A ⊆ A := by exact?

It gives me back exact Subset.rfl (correctly), but the Try this: turns the proof into := by exact Subset.rfl. I remember that Lean 3 library_search and similar could detect this kind of thing and make the proof := Subset.rfl. Is this something we can easily do with exact? and apply??

[Alex J. Best]

Sure you can do

import Mathlib.Tactic

example : x < x + 1 := exact?%

this isn't exactly answering your question of course, but hopefully its useful enough anyway :wink:

[Bhavik Mehta]

It is! You solved the #xy problem I didn't know I had :)

[Eric Rodriguez]

how does this magic work?

[Adam Topaz]

@Eric Rodriguez the exact?% term elaborator is defined here: https://github.com/leanprover-community/mathlib4/blob/7f885ee905fe01646967a99b54028c3270cce975/Mathlib/Tactic/LibrarySearch.lean#L289