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.