This is a list of the output of #help command of mathlib4. see GitHub Page!
This is heavily inspired by haruhisa-enomoto/mathlib4-all-tactics.
This web page is automatically updated by GitHub Action.
First, install Lean and Python 3.10, and then run the following commands:
rm .\src\tactics.md
lake env lean --run Tactic.lean > src/tactics.md
python3 script.py