タクティクの説明

https://leanprover.github.io/reference/tactics.htmlを見ても、自然言語で書いてあるだけ。これでは分からない！！

順行リーズニングと逆行リーズニングをペアにして、絵で説明しないと。