タクティク

タクティクは、Lean において証明を対話的に行ったり自動化したりすることを可能にするものです。

なおこのリストは全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば Mathlib4 Help を参照してください。