Mathlib Manual🔗

This document has been last updated at 2025-02-11 19:11 (+0000) using Lean 4.17.0-rc1 and Mathlib commit 6fec5f0.

Other resources:

If you would like to contribute content, please create a PR using the two github links at the bottom left of this page!

  1. 1. Tactics
    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