'Try this' tactic macro

This is a convenient shorthand intended for macro authors to be able to generate "Try this" recommendations. (It is not the main implementation of 'Try this', which is implemented in Lean core, see Lean.Meta.Tactic.TryThis.)

def Mathlib.Tactic.tacticTry_this_ : Lean.ParserDescr

Produces the text Try this: <tac> with the given tactic, and then executes it.

Equations

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

def Mathlib.Tactic.convTry_this_ : Lean.ParserDescr

Produces the text Try this: <tac> with the given conv tactic, and then executes it.

Equations

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