お久しぶりです．
Lean は安全性にパラメータを振りまくった純粋関数型プログラミング言語です．どのくらい安全性に振っているかというと，
配列にアクセスするときに，インデックスが配列の範囲内にあることの証明を引数として渡さないといけなかったり，
関数を定義するときに，関数が有限時間で停止することの証明を求められたり，
という感じです．
その結果として，別に定理証明をしようと思っていなくても，Lean を書くなら証明を避けて通ることはできません．そして，Lean の証明は Idris 等と異なりタクティクを使うことが多いでしょう．
そこで，参照に便利な Lean タクティクリストを lean-ja から公開しました．
実はまだベータ版であり誤りを含む可能性がありますが，コード例もたくさんつけましたし，十分初心者の役に立てると思います．「普段の数学でやってるアレはLeanでどうするのかな」という疑問に結構応えられるよう，日本語のひとこと説明を見出しに付記しておきました．
よろしければ使ってみてください．
