Hi, I am learning Lean4 for the purpose of LLM accelerated proof writing, thank you so so much for writing this book and posting it online open sourced. This book is easier than the other several books mentioned in the Lean4 official documentations and it comes with more examples and a more comfortable learning curve.

In short I want to let LLMs learn to master this language and freely translate between natural language and Lean4 for starter. As I am reading through this book I realize that for me the biggest issue is to "locate which tactic or theorem to use". Most of the time I know the next steps of the correct proves, yet I don't know how to express it in Lean4, same as the LLM we are training. (For example from t^2 = 0 to t = 0 when t in Real requires a tactic called pow_eq_zero and this wasn't mentioned anywhere, I looked up Cancel.Lean manually to spot it). Is it possible to formulate a quick cheatsheet that list all possible tactics and briefly discuss when they are applicable? Thanks!