We provide a single Lean file with 762 lines that teaches Lean tactic writing. If you are interested in Lean tactic writing, we assume you already know Lean, and probably use VS Code, in that case clone this repository, or simply download the file.

Alternatively, you can also copy it to Lean 4 Web but you will miss the Ctrl-click feature.

We tried to explain all the basic concepts but keep it beginner friendly. Enjoy learning Lean metaprogramming. If you are getting confused somewhere, it is probably not your fault. Let us know what needs more clarification in the Zulip thread.