# Documentation

Mathlib.Tactic.Find

# 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 applyable against the current goal.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.