Lean4 の主要なタクティクを使いたい場面から逆引きできるようにまとめたリストです．Lean4 で数学理論の形式化をする際に使われる主要なライブラリである，mathlib のタクティクも紹介しています．
誤りの指摘，編集の提案や寄稿を歓迎いたします．この GitHubリポジトリに issue や Pull Request を開いてください．
- 句読点は
,.を使用します． - タクティク
tacticに対して，記事の名前はtactic: (日本語による一言説明)とします． src/SUMMARY.mdのタクティク記事は，アルファベット昇順に並べてください．VSCode だとTyriar.sort-linesという拡張機能があって，並び替えを自動で行うことができます．- Lean コードは，コンパイルが通るようにして
Examples配下に配置します．「タクティクが失敗する例」を紹介したいときであってもtryや#guard_msgsなどを使ってコンパイルが通るようにしてください．コード例が正しいかチェックする際にその方が楽だからです． - 本文の markdown ファイルは mdgen を用いて lean ファイルから生成します．lean ファイルを編集した後，
lake run buildコマンドを実行すれば markdown の生成とmdbook buildが一括実行されます．
このプロジェクトは Proxima Technology 様よりご支援を頂いています.
Proxima Technology（プロキシマテクノロジー）は数学の社会実装を目指し, その⼀環としてモデル予測制御の民主化を掲げているAIスタートアップ企業です．数理科学の力で社会を変えることを企業の使命としています．