mathlib documentation

tactic.find

meta def expr.get_pis  :

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.

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.