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

Equations

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

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

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, the #find tactic can be used instead. There is also 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.

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

Display theorems (and definitions) whose result type matches the current goal, i.e. which should be applyable.

example : True := by find

find will not affect the goal by itself and should be removed from the finished proof. For a command that takes the type to search for as an argument, see #find, which is also available as a tactic.

Equations

• Mathlib.Tactic.Find.tacticFind = Lean.ParserDescr.node `Mathlib.Tactic.Find.tacticFind 1024 (Lean.ParserDescr.nonReservedSymbol "find" false)

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

The #find tactic finds definitions & lemmas using pattern matching on the type. For instance:

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

This is the tactic equivalent to the #find command. There is also 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.