tactic.find - mathlib docs

meta def expr.get_pis :

meta def pexpr.get_uninst_pis :

meta def find_cmd (_x : interactive.parse (lean.parser.tk "#find")) :

The find command from tactic.find allows to find definitions lemmas using pattern matching on the type. For instance:

import tactic.find

run_cmd tactic.skip

#find _ + _ = _ + _
#find (_ : ℕ) + _ = _ + _
#find ℕ → ℕ

The tactic library_search is an alternate way to find lemmas in the library.