Transitioning to mainstream Lean
If you have enjoyed this book, you may wish to work further with Lean, for example by working through the book Mathematics in Lean or by starting an independent formalization project.
You will discover that the Lean “dialect” used in this book differs from the mainstream mathematical Lean used in the library mathlib and its associated literature such as Mathematics in Lean. To help you adjust, in this appendix I outline the major differences.
Some tactics used in this book are deliberately weakened versions of tactics in mathlib: I have done this to block certain of Lean’s capabilities because prose proofs at the level of this book would typically write out the details in full. These deliberately weakened tactics include:
mathlib tactic 
weakened Mechanics of Proof version 
differences 



the reader to carry out by hand, including reduction mod \(n\), handling logic, and checking divisibility and primality 


substituting 


as adding/subtracting constants, it can combine many linear inequalities, and it does not require you to state which hypotheses you are using 


quantifierfree ones 
Some tactics used in this book have no mathlib analogues. They are typically wrappers for a small collection of lemmas, and in mathlib these lemmas would be invoked by name.
Mechanics of Proof tactic 
lemmas wrapped 






with the tactics 
Many of the problems in this book would be solved much more efficiently in mathlibstyle Lean, because there is some sequence of steps which can be carried out as one step by an advanced algorithm which is beyond the mathematical scope of this book. Some tactics of this kind to be aware of:
algorithm 
mathlib tactic 
the kinds of steps this tactic can replace 








logic tactics at the end of a proof or subproof 
Another point not covered in this book is how to interact with the library. Since mathlib contains over a million lines of Lean code, it is not always easy to find out whether a lemma you want exists in the library! In this book, I avoid the issue by telling you in advance the name of any lemma I expect you to use.
A few basic points to be aware of in interacting with the library:
The online documentation is generally more readable than the source code: it is searchable and it has internal hyperlinks.
Lemmas are often stated in extreme generality … \((a  b) + c = a  (b  c)\) is stated not for \(\mathbb{R}\) but for a
SubtractionCommMonoid
. You may have better luck interacting with the library after first courses on abstract algebra and pointset topology.If you can guess the exact statement of a lemma, the tactic
exact?
will find it in the library.
All this only scratches the surface: there are many more features of Lean to help you in your mathematical discoveries. Mathematics in Lean, the community website, and the community discussion board offer further pointers for exploration. Have fun!