Documentation on all tactics

Stream: Is there code for X?

[Hanting Zhang]

I haven't used Lean in a while, but back then I remember there was a nice document listing all the tactics with an explanation of how to use it, tips and tricks, etc. Does this still exist somewhere, or has it been moved into a more structured place, or in general is there somewhere that contains something like this? Thanks!

[Jason Rute]

https://proofassistants.stackexchange.com/questions/3986/is-there-a-complete-index-of-lean-4-tactics

[Asei Inoue]

here: https://seasawher.github.io/mathlib4-help/