既存 project に Mathlib を追加する

すでにある Lean project に Mathlib を追加するには，Lean バージョンと Mathlib のバージョンを揃える必要があります． Mathlib は Lean 本体の特定バージョンに依存しているため，適当な Lean バージョンと適当な Mathlib revision を混ぜると， lake update や import Mathlib でエラーになります．

この資料のように lakefile.toml を使う場合，たとえば Lean 4.30.0 に対応する Mathlib release を使うなら， lean-toolchain を次のようにします．

leanprover/lean4:v4.30.0

そして lakefile.toml に Mathlib の依存関係を追加します．

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.30.0"

追加後，project ルートで次を実行します．

lake update
lake exe cache get
lake build

lakefile.lean を使う project なら，依存関係は次のように書きます．

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0"

Mathlib の最新版 master に追随する場合は，Mathlib 側の lean-toolchain に Lean バージョンを合わせます．

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

ただし，講義資料や共同研究では，毎回 master に追随するより，特定の release tag や commit hash に固定する方が安定です．