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 : Batteries.Tactic.DeclCache (Std.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

#find t finds definitions and theorems whose result type matches the term t, and prints them as info lines. Use holes in t to indicate arbitrary subexpressions, for example #find _ ∧ _ will match any conjunction.

#find is also available as a tactic, and there is also the find tactic which looks for lemmas which are applyable against the current goal.

Examples:

#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat

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

find finds definitions and theorems whose result type matches the current goal exactly, and prints them as info lines. In other words, find lists definitions and theorems that are applyable against the current goal. find will not affect the goal by itself and should be removed from the finished proof.

For a command or tactic that takes the type to search for as an argument, see #find.

Example:

example : True := by
  find
  -- True.intro: True
  -- trivial: True
  -- ...

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

#find t finds definitions and theorems whose result type matches the term t, and prints them as info lines. Use holes in t to indicate arbitrary subexpressions, for example #find _ ∧ _ will match any conjunction. #find is also available as a command. #find will not affect the goal by itself and should be removed from the finished proof.

There is also the find tactic which looks for lemmas which are applyable against the current goal.

Examples:

#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat