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.

opaque Mathlib.Tactic.Find.findDeclsPerHead : Mathlib.Tactic.DeclCache (Lean.HashMap Lean.HeadIndex (Array Lean.Name))

def Mathlib.Tactic.Find.findType (t : Lean.Expr) : Lean.Elab.TermElabM Unit

def Mathlib.Tactic.Find.«command#find_» : Lean.ParserDescr

def Mathlib.Tactic.Find.tacticFind : Lean.ParserDescr

def Mathlib.Tactic.Find.«tactic#find_» : Lean.ParserDescr