ドキュメントを流し読みしているのが一番悪いとはいえMathlib4の証明を読んで「こんなtacticsあるんだ」みたいな発見をすることが多々あり、さておきLean4のドキュメントは利用例も含めて少なすぎるので、日本語圏での普及を目的として何かしらのWikiとかを作って啓蒙/連帯したすぎる