1. Tactics
This chapter introduces many tactics that are used to proof theorems.
A tactic proof is started using by
.
The last section contains an automatically generated list of all tactics known to Mathlib, the sections before that are manually curated.
The displayed tactic names and docstring are automatically extracted from the Lean code, so if the information is wrong, you should directly create a PR to the repo containing the tactic and change things there.
The section prior to the last section are not final in any way. Feel free to add/delete/rename/restructure any of these section and modify their content freely to make them more useful! PR go to the repository of this manual.