tryAtEachStep is a tool that runs a tactic at every proof step in a given Lean 4 file, reporting cases where the tactic closes the goal.

With a tactic like exact? and rw_search, this can help to find ways in which your existing proofs can be improved.


Add this to your lakefile.lean:

require tryAtEachStep from git "" @ "main"

Then do this:

$ lake exe tryAtEachStep exact? Foo/Bar.lean

Example findings:


  • Tests
  • Run in parallel on all .lean files in a project.
  • Support tactics that aren't imported by the input file.
  • Better handling of situations where there are multiple active goals.
  • Report performance statistics of existing and new tactic.
  • Operate on terms. (Currently only operates on the tactic steps of the given file.)