Theorem Proving in Lean 4 日本語訳 Theorem Proving in Lean 4 日本語訳 イントロダクション 依存型理論 命題と証明 量化子と等号 タクティク Leanとの対話 帰納型 帰納と再帰 構造体とレコード 型クラス 変換タクティクモード 公理と計算