mathlib documentation

tactic.tidy

Tag interactive tactics (locally) with [tidy] to add them to the list of default tactics called by tidy.

meta structure tactic.tidy.cfg  :
Type

Use a variety of conservative tactics to solve goals.

tidy? reports back the tactic script it found. As an example

example :  x : unit, x = unit.star :=
begin
  tidy? -- Prints the trace message: "Try this: intros x, exact dec_trivial"
end

The default list of tactics is stored in tactic.tidy.default_tidy_tactics. This list can be overridden using tidy { tactics := ... }. (The list must be a list of tactic string, so that tidy? can report a usable tactic script.)

Tactics can also be added to the list by tagging them (locally) with the [tidy] attribute.

Invoking the hole command tidy ("Use tidy to complete the goal") runs the tactic of the same name, replacing the hole with the tactic script tidy produces.