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.

  1. 1.1. Interactive
  2. 1.2. Automation
  3. 1.3. Algebra
  4. 1.4. Analysis
  5. 1.5. Coercions
  6. 1.6. Category Theory
  7. 1.7. Logic
  8. 1.8. Induction / case distinction
  9. 1.9. Basic tactics / assumptions
  10. 1.10. Definitional equality
  11. 1.11. Conv mode
  12. 1.12. Control flow
  13. 1.13. For Tests
  14. 1.14. Miscellaneous
  15. 1.15. All tactics