The #find
command and tactic. #
The #find
command finds definitions & lemmas using pattern matching on the type. For instance:
#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat
Inside tactic proofs, there is a #find
tactic with the same syntax,
or the find
tactic which looks for lemmas which are apply
able against the current goal.