From afe5267fcc2f55d77f265d94defaff65a2e03299 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 04:43:33 +0900
Subject: [PATCH 01/17] =?UTF-8?q?Windows=E3=81=A7=E3=81=AE=E3=82=A4?=
 =?UTF-8?q?=E3=83=B3=E3=82=B9=E3=83=88=E3=83=BC=E3=83=ABDocker=20file=20?=
 =?UTF-8?q?=E3=81=AE=E3=83=86=E3=82=B9=E3=83=88?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 34 ++++++++++++++++++++++++++++++++++
 Docker/Dockerfile.win         |  8 ++++++++
 Docker/README.md              | 19 +++++++++++++++++++
 3 files changed, 61 insertions(+)
 create mode 100644 .github/workflows/install.yml
 create mode 100644 Docker/Dockerfile.win
 create mode 100644 Docker/README.md

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
new file mode 100644
index 00000000..dd069df5
--- /dev/null
+++ b/.github/workflows/install.yml
@@ -0,0 +1,34 @@
+name: Validate install procedure
+
+on:
+  pull_request:
+    branches:
+      - main
+    paths:
+      - 'Docker/**'
+      - '.github/workflows/install.yml'
+  push:
+    branches:
+      - main
+    paths:
+      - 'Docker/**'
+      - '.github/workflows/install.yml'
+  schedule:
+    - cron: "0 0 1 * *"
+  workflow_dispatch:
+
+jobs:
+  validate_for_windows:
+    runs-on: windows-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v6
+
+      - name: build windows container
+        shell: pwsh
+        run: |
+          docker build `
+            --progress=plain `
+            --file Docker/Dockerfile.win `
+            --tag win-test:latest `
+            .
diff --git a/Docker/Dockerfile.win b/Docker/Dockerfile.win
new file mode 100644
index 00000000..4d53a858
--- /dev/null
+++ b/Docker/Dockerfile.win
@@ -0,0 +1,8 @@
+FROM mcr.microsoft.com/powershell:windowsservercore-ltsc2022
+
+# PowerShell 7 を使う
+SHELL ["pwsh", "-Command"]
+
+# 依存関係がインストールされていることを確認する
+RUN git --version
+RUN curl --version
diff --git a/Docker/README.md b/Docker/README.md
new file mode 100644
index 00000000..9e1c655c
--- /dev/null
+++ b/Docker/README.md
@@ -0,0 +1,19 @@
+# README
+
+これは、Lean(正確には elan, lake, lean) のインストール手順を検証するための Dockerfile です。
+
+## 使い方
+
+Dockerfile をビルドしてイメージを作成するには、以下のコマンドを実行します。
+
+```bash
+docker build \
+  --file Docker/Dockerfile.xxx \
+  --tag install-lean:xxx .
+```
+
+ビルドしたイメージを使ってコンテナを起動し、中に入ってコマンドを実行するには以下を実行します。
+
+```bash
+docker run --rm -it install-lean:xxx bash
+```

From 8b4c22359f1ad6760fd15665c26b4e43649f5716 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 04:45:51 +0900
Subject: [PATCH 02/17] =?UTF-8?q?=E5=BE=AE=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index dd069df5..3708a15a 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -28,7 +28,6 @@ jobs:
         shell: pwsh
         run: |
           docker build `
-            --progress=plain `
             --file Docker/Dockerfile.win `
             --tag win-test:latest `
             .

From 6046ea8fd7241670a8c2d34be7641bbb22198a59 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:01:17 +0900
Subject: [PATCH 03/17] =?UTF-8?q?=E4=BF=AE=E6=AD=A3.=20Dockerfile=20?=
 =?UTF-8?q?=E3=82=92=E4=BD=BF=E3=82=8F=E3=81=9A=E3=80=81=E6=9C=80=E5=88=9D?=
 =?UTF-8?q?=E3=81=8B=E3=82=89=20GitHub=20Action=20=E3=81=A7=E3=83=86?=
 =?UTF-8?q?=E3=82=B9=E3=83=88=E3=82=92=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 30 +++++++++++++++++++++++-------
 Docker/Dockerfile.win         |  8 --------
 2 files changed, 23 insertions(+), 15 deletions(-)
 delete mode 100644 Docker/Dockerfile.win

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 3708a15a..f333f40b 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -1,4 +1,4 @@
-name: Validate install procedure
+name: validate installation procedure
 
 on:
   pull_request:
@@ -18,16 +18,32 @@ on:
   workflow_dispatch:
 
 jobs:
-  validate_for_windows:
+  install_lean_for_windows:
     runs-on: windows-latest
     steps:
       - name: checkout
         uses: actions/checkout@v6
 
-      - name: build windows container
+      - name: check dependencies
         shell: pwsh
         run: |
-          docker build `
-            --file Docker/Dockerfile.win `
-            --tag win-test:latest `
-            .
+          git --version
+          curl --version
+
+      - name: install elan
+        shell: pwsh
+        run: |
+          curl -O --location https://elan.lean-lang.org/elan-init.ps1
+          pwsh `
+            -ExecutionPolicy Bypass `
+            -f elan-init.ps1 `
+            -NoPrompt:$True `
+            -DefaultToolchain:beta
+          Remove-Item elan-init.ps1
+
+      - name: check installation
+        shell: pwsh
+        run: |
+          lean --version
+          lake --version
+          elan --version
diff --git a/Docker/Dockerfile.win b/Docker/Dockerfile.win
deleted file mode 100644
index 4d53a858..00000000
--- a/Docker/Dockerfile.win
+++ /dev/null
@@ -1,8 +0,0 @@
-FROM mcr.microsoft.com/powershell:windowsservercore-ltsc2022
-
-# PowerShell 7 を使う
-SHELL ["pwsh", "-Command"]
-
-# 依存関係がインストールされていることを確認する
-RUN git --version
-RUN curl --version

From 06a33c1375b42fbc8308b6742a80cf60caeb5314 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:05:56 +0900
Subject: [PATCH 04/17] =?UTF-8?q?PATH=20=E3=81=AB=E8=BF=BD=E5=8A=A0?=
 =?UTF-8?q?=E3=81=99=E3=82=8B=E3=82=B9=E3=83=86=E3=83=83=E3=83=97=E3=82=92?=
 =?UTF-8?q?=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index f333f40b..c70df105 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -41,6 +41,11 @@ jobs:
             -DefaultToolchain:beta
           Remove-Item elan-init.ps1
 
+      - name: modify PATH
+        shell: pwsh
+        run: |
+          Add-Content -Path $env:GITHUB_PATH -Value "$env:USERPROFILE\.elan\bin"
+
       - name: check installation
         shell: pwsh
         run: |

From 0e1df28499b95286f1cebc1373ff859c8406624f Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:12:36 +0900
Subject: [PATCH 05/17] =?UTF-8?q?=E4=BF=AE=E6=AD=A3=E3=80=82=E6=98=8E?=
 =?UTF-8?q?=E7=A4=BA=E7=9A=84=E3=81=AB=20elan=20toolchain=20=E3=82=B3?=
 =?UTF-8?q?=E3=83=9E=E3=83=B3=E3=83=89=E3=81=A7=E3=82=A4=E3=83=B3=E3=82=B9?=
 =?UTF-8?q?=E3=83=88=E3=83=BC=E3=83=AB=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index c70df105..b8441212 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -46,9 +46,18 @@ jobs:
         run: |
           Add-Content -Path $env:GITHUB_PATH -Value "$env:USERPROFILE\.elan\bin"
 
-      - name: check installation
+      - name: check installation of elan
+        shell: pwsh
+        run: elan --version
+
+      - name: install latest beta version of Lean
+        shell: pwsh
+        run: |
+          elan default beta
+          elan toolchain install beta
+
+      - name: check installation of Lean and lake
         shell: pwsh
         run: |
           lean --version
           lake --version
-          elan --version

From 87fd235b807ea11482f1fed5c34c11506e130aa8 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:13:05 +0900
Subject: [PATCH 06/17] =?UTF-8?q?=E5=89=8A=E9=99=A4=E5=BF=98=E3=82=8C?=
 =?UTF-8?q?=E3=82=92=E5=89=8A=E9=99=A4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index b8441212..fec4aa79 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -37,8 +37,7 @@ jobs:
           pwsh `
             -ExecutionPolicy Bypass `
             -f elan-init.ps1 `
-            -NoPrompt:$True `
-            -DefaultToolchain:beta
+            -NoPrompt:$True
           Remove-Item elan-init.ps1
 
       - name: modify PATH

From 4d8becb4eceb119f7da9010f5f21e729506dc58f Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:21:24 +0900
Subject: [PATCH 07/17] =?UTF-8?q?=E3=83=93=E3=83=AB=E3=83=89=E3=81=BE?=
 =?UTF-8?q?=E3=81=A7=E3=83=86=E3=82=B9=E3=83=88=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index fec4aa79..853ba282 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -60,3 +60,15 @@ jobs:
         run: |
           lean --version
           lake --version
+
+      - name: check build
+        shell: pwsh
+        run: |
+          lake new Test lib.lean
+          cd Test
+
+          @'
+          #eval "Lean 言語をはじめよう 🐙🦈"
+          '@ | Set-Content -Path .\Test\Basic.lean -Encoding utf8
+
+          lake build

From 8dd1df1dec85d4fbcc2a196a4517906fe0ba92be Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:27:10 +0900
Subject: [PATCH 08/17] =?UTF-8?q?`checkout`=20=E3=82=A2=E3=82=AF=E3=82=B7?=
 =?UTF-8?q?=E3=83=A7=E3=83=B3=E3=82=92=E6=8A=9C=E3=81=84=E3=81=A6=E3=81=97?=
 =?UTF-8?q?=E3=81=BE=E3=81=86?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 853ba282..70862a03 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -21,9 +21,6 @@ jobs:
   install_lean_for_windows:
     runs-on: windows-latest
     steps:
-      - name: checkout
-        uses: actions/checkout@v6
-
       - name: check dependencies
         shell: pwsh
         run: |

From ea14fcb6e3a9a4e87a8bd0062eb69c460c7c076a Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 05:33:31 +0900
Subject: [PATCH 09/17] =?UTF-8?q?build=20=E9=83=A8=E5=88=86=E3=81=AF?=
 =?UTF-8?q?=E5=89=8A=E9=99=A4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 70862a03..a67828d2 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -57,15 +57,3 @@ jobs:
         run: |
           lean --version
           lake --version
-
-      - name: check build
-        shell: pwsh
-        run: |
-          lake new Test lib.lean
-          cd Test
-
-          @'
-          #eval "Lean 言語をはじめよう 🐙🦈"
-          '@ | Set-Content -Path .\Test\Basic.lean -Encoding utf8
-
-          lake build

From e23a5b3c2d8e8ea8f9cb82e35dd614478e7db23a Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 06:31:45 +0900
Subject: [PATCH 10/17] =?UTF-8?q?=E3=82=A4=E3=83=B3=E3=82=B9=E3=83=88?=
 =?UTF-8?q?=E3=83=BC=E3=83=AB=E6=96=B9=E6=B3=95=E3=81=AE=E6=A1=88=E5=86=85?=
 =?UTF-8?q?=E3=82=92=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml   |   6 +-
 LeanByExample/HowToInstall.lean | 107 ++++++++++++++++++++++++++++++++
 booksrc/SUMMARY.md              |   1 +
 3 files changed, 111 insertions(+), 3 deletions(-)
 create mode 100644 LeanByExample/HowToInstall.lean

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index a67828d2..91cdf2a6 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -46,11 +46,11 @@ jobs:
         shell: pwsh
         run: elan --version
 
-      - name: install latest beta version of Lean
+      - name: install latest stable version of Lean
         shell: pwsh
         run: |
-          elan default beta
-          elan toolchain install beta
+          elan default stable
+          elan toolchain install stable
 
       - name: check installation of Lean and lake
         shell: pwsh
diff --git a/LeanByExample/HowToInstall.lean b/LeanByExample/HowToInstall.lean
new file mode 100644
index 00000000..ba8595ef
--- /dev/null
+++ b/LeanByExample/HowToInstall.lean
@@ -0,0 +1,107 @@
+/- # Lean のインストール方法
+
+Lean および関連ツールのインストール方法を説明します。VSCode の Lean 4 拡張機能が自動的にインストールしてくれるのですが、ここでは手動で入れる場合の手順を説明します。
+
+## Windows の場合
+
+### PowerShell 7 のインストール
+
+まずは使用しているシェルを確認します。[PowerShell 7](https://github.com/PowerShell/PowerShell) を使うことを推奨します。他のシェルでも Lean のインストール自体は可能ですが、Windows では PowerShell 7 を使うことが一般的であるためこのような手順を案内しています。
+
+Windows PowerShell と PowerShell 7 以降は混同されがちですが、下記を実行して Major が 7 以上であれば PowerShell 7 です。
+
+```powershell
+$PSVersionTable.PSVersion
+```
+
+PowerShell 7 をインストールするには、次を実行します。
+
+```powershell
+winget install --id Microsoft.PowerShell --source winget
+```
+
+### git と curl のインストール
+
+以下、全てのコマンドは PowerShell 7 で実行することを前提とすることにします。
+
+Lean のインストールのためには `git` コマンドと `curl` コマンドが必要です。`git` はテキストのバージョン管理をするためのツールで、`curl` はデータを外部から取得したり、外部に送信したりするためのツールです。
+
+それぞれインストール済みであるか、次のコマンドで確認します。
+
+```powershell
+git --version
+curl --version
+```
+
+おそらく初期状態の Windows では `git` はインストールされていないと思います。以下のコマンドでインストールします。
+
+```powershell
+winget install --id Git.Git -e --source winget
+```
+
+`curl` コマンドはおそらく初めから入っていると思いますが、もし入っていない場合は次のコマンドでインストールします。
+
+```powershell
+winget install --id cURL.cURL --source winget
+```
+
+### elan のインストール
+
+次に、Lean のバージョン管理ツールである `elan` をインストールします。次のコマンドでインストールできます。
+
+```powershell
+curl -O --location https://elan.lean-lang.org/elan-init.ps1
+pwsh `
+  -ExecutionPolicy Bypass `
+  -f elan-init.ps1 `
+  -NoPrompt:$True
+Remove-Item elan-init.ps1
+```
+
+実行後、`elan` コマンドが使えるようになったか確認します。
+
+```powershell
+elan --version
+```
+
+### Lean のインストール
+
+次に、Lean をインストールします。`stable` を指定することで、最新の安定版をインストールできます。
+
+```powershell
+elan toolchain install stable
+```
+
+もし、`-rc` 系も含めた最新版をインストールしたい場合は、次のようにします。
+
+```powershell
+elan toolchain install beta
+```
+
+終わったら、Lean のバージョンを確認します。
+
+```powershell
+lean --version
+```
+
+### プロジェクト作成
+
+Lean をインストールすると、Lean のパッケージ管理ツールである `lake` もインストールされます。
+
+```powershell
+lake --version
+```
+
+`lake new` コマンドを使うと、Lean のプロジェクトを作成することができます。
+
+```powershell
+lake new TestProject
+```
+
+ビルドが正常に実行できることを確認しておきましょう。
+
+```powershell
+cd TestProject
+lake build
+```
+-/
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 4dee0966..a5118f4f 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -3,6 +3,7 @@
 [はじめに](./README.md)
 
 [リンク集](./Links.md)
+[Leanのインストール方法](./HowToInstall.md)
 [Mathlib4 Help](./Mathlib4Help.md)
 [ランダムページ](./Random.md)
 

From 477c82dfeaab75fa0d75808dd7a516b91baade99 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 06:37:45 +0900
Subject: [PATCH 11/17] =?UTF-8?q?Docker=20=E3=83=87=E3=82=A3=E3=83=AC?=
 =?UTF-8?q?=E3=82=AF=E3=83=88=E3=83=AA=E3=82=92=E4=BD=BF=E7=94=A8=E3=81=97?=
 =?UTF-8?q?=E3=81=AA=E3=81=84?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml |  2 --
 Docker/README.md              | 19 -------------------
 2 files changed, 21 deletions(-)
 delete mode 100644 Docker/README.md

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 91cdf2a6..555faa08 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -5,13 +5,11 @@ on:
     branches:
       - main
     paths:
-      - 'Docker/**'
       - '.github/workflows/install.yml'
   push:
     branches:
       - main
     paths:
-      - 'Docker/**'
       - '.github/workflows/install.yml'
   schedule:
     - cron: "0 0 1 * *"
diff --git a/Docker/README.md b/Docker/README.md
deleted file mode 100644
index 9e1c655c..00000000
--- a/Docker/README.md
+++ /dev/null
@@ -1,19 +0,0 @@
-# README
-
-これは、Lean(正確には elan, lake, lean) のインストール手順を検証するための Dockerfile です。
-
-## 使い方
-
-Dockerfile をビルドしてイメージを作成するには、以下のコマンドを実行します。
-
-```bash
-docker build \
-  --file Docker/Dockerfile.xxx \
-  --tag install-lean:xxx .
-```
-
-ビルドしたイメージを使ってコンテナを起動し、中に入ってコマンドを実行するには以下を実行します。
-
-```bash
-docker run --rm -it install-lean:xxx bash
-```

From 5a25c10caff5d5664c4faad1d490a5295ffe2387 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 14:35:38 +0900
Subject: [PATCH 12/17] =?UTF-8?q?Linux=20=E3=81=A7=E3=81=AE=E6=89=8B?=
 =?UTF-8?q?=E9=A0=86=E3=82=92=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml   | 35 +++++++++++++++++++
 LeanByExample/HowToInstall.lean | 61 ++++++++++++++++++++++++++-------
 2 files changed, 84 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 555faa08..ff01679c 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -55,3 +55,38 @@ jobs:
         run: |
           lean --version
           lake --version
+
+  install_lean_for_linux:
+    runs-on: ubuntu-latest
+    steps:
+      - name: check dependencies
+        shell: bash
+        run: |
+          git --version
+          curl --version
+
+      - name: install elan
+        shell: bash
+        run: |
+          curl -O --location https://elan.lean-lang.org/elan-init.sh
+          sh elan-init.sh -y --default-toolchain stable
+          rm elan-init.sh
+
+      - name: modify PATH
+        shell: bash
+        run: echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: check installation of elan
+        shell: bash
+        run: elan --version
+
+      - name: install latest stable version of Lean
+        shell: bash
+        run: |
+          elan toolchain install stable
+
+      - name: check installation of Lean and lake
+        shell: bash
+        run: |
+          lean --version
+          lake --version
diff --git a/LeanByExample/HowToInstall.lean b/LeanByExample/HowToInstall.lean
index ba8595ef..797feb99 100644
--- a/LeanByExample/HowToInstall.lean
+++ b/LeanByExample/HowToInstall.lean
@@ -1,6 +1,6 @@
 /- # Lean のインストール方法
 
-Lean および関連ツールのインストール方法を説明します。VSCode の Lean 4 拡張機能が自動的にインストールしてくれるのですが、ここでは手動で入れる場合の手順を説明します。
+Lean および関連ツールのインストール方法を説明します。VSCode の Lean 4 拡張機能が自動的にインストールしてくれるのですが、ここではコマンドラインから手動で入れる場合の手順を説明します。
 
 ## Windows の場合
 
@@ -64,9 +64,9 @@ Remove-Item elan-init.ps1
 elan --version
 ```
 
-### Lean のインストール
+### Lean と lake のインストール
 
-次に、Lean をインストールします。`stable` を指定することで、最新の安定版をインストールできます。
+次に、Lean（と同梱されている `lake`）をインストールします。`stable` を指定することで、最新の安定版をインストールできます。
 
 ```powershell
 elan toolchain install stable
@@ -78,30 +78,67 @@ elan toolchain install stable
 elan toolchain install beta
 ```
 
-終わったら、Lean のバージョンを確認します。
+終わったら、Lean と `lake` のバージョンを確認します。
 
 ```powershell
 lean --version
+lake --version
+```
+
+## Linux の場合
+
+だいたい Windows での手順と同様です。シェルは `bash` を使用することを想定して手順を書きます。
+
+### git と curl のインストール
+
+まず、`git` と `curl` がインストール済みであるか確認します。
+
+```bash
+git --version
+curl --version
+```
+
+インストールされていなければインストールします。
+
+```bash
+sudo apt update
+sudo apt install -y git curl
+```
+
+### elan のインストール
+
+次に `elan` をインストールします。
+
+```bash
+curl -O --location https://elan.lean-lang.org/elan-init.sh
+sh elan-init.sh -y --default-toolchain stable
+rm elan-init.sh
+```
+
+終わったら `elan` コマンドが使えるようになったか確認します。
+
+```bash
+elan --version
 ```
 
-### プロジェクト作成
+### Lean と lake のインストール
 
-Lean をインストールすると、Lean のパッケージ管理ツールである `lake` もインストールされます。
+次に、Lean（と同梱されている `lake`）をインストールします。`stable` を指定することで、最新の安定版をインストールできます。
 
 ```powershell
-lake --version
+elan toolchain install stable
 ```
 
-`lake new` コマンドを使うと、Lean のプロジェクトを作成することができます。
+もし、`-rc` 系も含めた最新版をインストールしたい場合は、次のようにします。
 
 ```powershell
-lake new TestProject
+elan toolchain install beta
 ```
 
-ビルドが正常に実行できることを確認しておきましょう。
+終わったら、Lean と `lake` のバージョンを確認します。
 
 ```powershell
-cd TestProject
-lake build
+lean --version
+lake --version
 ```
 -/

From 786db42550dd3df92051137000308e5a3fef5982 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 14:39:11 +0900
Subject: [PATCH 13/17] =?UTF-8?q?=E5=AE=9F=E8=A1=8C=E3=82=BF=E3=82=A4?=
 =?UTF-8?q?=E3=83=9F=E3=83=B3=E3=82=B0=E3=82=92=E3=81=9D=E3=82=8D=E3=81=88?=
 =?UTF-8?q?=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/devcontainer.yml | 2 +-
 .github/workflows/update.yml       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/devcontainer.yml b/.github/workflows/devcontainer.yml
index 6932a962..ff3b6bef 100644
--- a/.github/workflows/devcontainer.yml
+++ b/.github/workflows/devcontainer.yml
@@ -14,7 +14,7 @@ on:
       - '.devcontainer/**'
       - '.github/workflows/devcontainer.yml'
   schedule:
-    - cron: "0 0 5 * *"
+    - cron: "0 0 1 * *"
   workflow_dispatch:
 
 jobs:
diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index e765ed52..b644809f 100644
--- a/.github/workflows/update.yml
+++ b/.github/workflows/update.yml
@@ -2,7 +2,7 @@ name: Update Lean
 on:
   schedule:
     # 毎日実行
-    - cron: "0 3 * * *"
+    - cron: "0 0 * * *"
   workflow_dispatch:
 
 permissions:

From f7810dbb02341b5412c78ba38adf0e280a3125e0 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 14:41:38 +0900
Subject: [PATCH 14/17] =?UTF-8?q?DefaultToolchain=20=E3=82=92=E6=8C=87?=
 =?UTF-8?q?=E5=AE=9A=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml   |  3 ++-
 LeanByExample/HowToInstall.lean | 15 ++-------------
 2 files changed, 4 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index ff01679c..b766de88 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -32,7 +32,8 @@ jobs:
           pwsh `
             -ExecutionPolicy Bypass `
             -f elan-init.ps1 `
-            -NoPrompt:$True
+            -NoPrompt:$True `
+            -DefaultToolchain:stable
           Remove-Item elan-init.ps1
 
       - name: modify PATH
diff --git a/LeanByExample/HowToInstall.lean b/LeanByExample/HowToInstall.lean
index 797feb99..151f9e29 100644
--- a/LeanByExample/HowToInstall.lean
+++ b/LeanByExample/HowToInstall.lean
@@ -54,7 +54,8 @@ curl -O --location https://elan.lean-lang.org/elan-init.ps1
 pwsh `
   -ExecutionPolicy Bypass `
   -f elan-init.ps1 `
-  -NoPrompt:$True
+  -NoPrompt:$True `
+  -DefaultToolchain:stable
 Remove-Item elan-init.ps1
 ```
 
@@ -72,12 +73,6 @@ elan --version
 elan toolchain install stable
 ```
 
-もし、`-rc` 系も含めた最新版をインストールしたい場合は、次のようにします。
-
-```powershell
-elan toolchain install beta
-```
-
 終わったら、Lean と `lake` のバージョンを確認します。
 
 ```powershell
@@ -129,12 +124,6 @@ elan --version
 elan toolchain install stable
 ```
 
-もし、`-rc` 系も含めた最新版をインストールしたい場合は、次のようにします。
-
-```powershell
-elan toolchain install beta
-```
-
 終わったら、Lean と `lake` のバージョンを確認します。
 
 ```powershell

From abb7534da13eea19176906f66a19ee7bd8a79e8b Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 14:56:41 +0900
Subject: [PATCH 15/17] =?UTF-8?q?MacOS=20=E3=81=A7=E3=81=AE=E3=82=A4?=
 =?UTF-8?q?=E3=83=B3=E3=82=B9=E3=83=88=E3=83=BC=E3=83=AB=E6=89=8B=E9=A0=86?=
 =?UTF-8?q?=E3=82=92=E6=9B=B8=E3=81=8F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml   | 36 ++++++++++++++++++++-
 LeanByExample/HowToInstall.lean | 56 +++++++++++++++++++++++++++++++--
 2 files changed, 88 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index b766de88..1c8fe39b 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -48,7 +48,6 @@ jobs:
       - name: install latest stable version of Lean
         shell: pwsh
         run: |
-          elan default stable
           elan toolchain install stable
 
       - name: check installation of Lean and lake
@@ -91,3 +90,38 @@ jobs:
         run: |
           lean --version
           lake --version
+
+  install_lean_for_mac:
+    runs-on: macos-latest
+    steps:
+      - name: check dependencies
+        shell: zsh
+        run: |
+          git --version
+          curl --version
+
+      - name: install elan
+        shell: zsh
+        run: |
+          curl -O --location https://elan.lean-lang.org/elan-init.sh
+          sh elan-init.sh -y --default-toolchain stable
+          rm elan-init.sh
+
+      - name: modify PATH
+        shell: zsh
+        run: echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: check installation of elan
+        shell: zsh
+        run: elan --version
+
+      - name: install latest stable version of Lean
+        shell: zsh
+        run: |
+          elan toolchain install stable
+
+      - name: check installation of Lean and lake
+        shell: zsh
+        run: |
+          lean --version
+          lake --version
diff --git a/LeanByExample/HowToInstall.lean b/LeanByExample/HowToInstall.lean
index 151f9e29..238f7e6a 100644
--- a/LeanByExample/HowToInstall.lean
+++ b/LeanByExample/HowToInstall.lean
@@ -82,7 +82,7 @@ lake --version
 
 ## Linux の場合
 
-だいたい Windows での手順と同様です。シェルは `bash` を使用することを想定して手順を書きます。
+シェルは `bash` を使用することを想定して手順を書きます。
 
 ### git と curl のインストール
 
@@ -120,13 +120,63 @@ elan --version
 
 次に、Lean（と同梱されている `lake`）をインストールします。`stable` を指定することで、最新の安定版をインストールできます。
 
-```powershell
+```bash
 elan toolchain install stable
 ```
 
 終わったら、Lean と `lake` のバージョンを確認します。
 
-```powershell
+```bash
+lean --version
+lake --version
+```
+
+## MacOS の場合
+
+シェルとして `zsh` を利用することを想定して手順を書きます。
+
+### git と curl のインストール
+
+MacOS の場合、`curl` は最初から入っていると思います。`git` が入っていない場合、次のコマンドでインストールできます。
+
+```zsh
+xcode-select --install
+```
+
+終わったら `git` と `curl` が使えるか確認します。
+
+```zsh
+git --version
+curl --version
+```
+
+### elan のインストール
+
+次に `elan` をインストールします。
+
+```zsh
+curl -O --location https://elan.lean-lang.org/elan-init.sh
+sh elan-init.sh -y --default-toolchain stable
+rm elan-init.sh
+```
+
+終わったら `elan` コマンドが使えるようになったか確認します。
+
+```zsh
+elan --version
+```
+
+### Lean と lake のインストール
+
+次に、Lean（と同梱されている `lake`）をインストールします。`stable` を指定することで、最新の安定版をインストールできます。
+
+```zsh
+elan toolchain install stable
+```
+
+終わったら、Lean と `lake` のバージョンを確認します。
+
+```zsh
 lean --version
 lake --version
 ```

From ad5b9e1182c1fd45261e27a1db7440bbe9a30077 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 14:59:34 +0900
Subject: [PATCH 16/17] =?UTF-8?q?=E3=82=B7=E3=82=A7=E3=83=AB=E3=81=AE?=
 =?UTF-8?q?=E6=8C=87=E5=AE=9A=E3=82=92=E5=A4=89=E3=81=88=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/install.yml | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 1c8fe39b..a4b90c0f 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -18,15 +18,16 @@ on:
 jobs:
   install_lean_for_windows:
     runs-on: windows-latest
+    defaults:
+      run:
+        shell: pwsh
     steps:
       - name: check dependencies
-        shell: pwsh
         run: |
           git --version
           curl --version
 
       - name: install elan
-        shell: pwsh
         run: |
           curl -O --location https://elan.lean-lang.org/elan-init.ps1
           pwsh `
@@ -37,91 +38,81 @@ jobs:
           Remove-Item elan-init.ps1
 
       - name: modify PATH
-        shell: pwsh
         run: |
           Add-Content -Path $env:GITHUB_PATH -Value "$env:USERPROFILE\.elan\bin"
 
       - name: check installation of elan
-        shell: pwsh
         run: elan --version
 
       - name: install latest stable version of Lean
-        shell: pwsh
         run: |
           elan toolchain install stable
 
       - name: check installation of Lean and lake
-        shell: pwsh
         run: |
           lean --version
           lake --version
 
   install_lean_for_linux:
     runs-on: ubuntu-latest
+    defaults:
+      run:
+        shell: bash
     steps:
       - name: check dependencies
-        shell: bash
         run: |
           git --version
           curl --version
 
       - name: install elan
-        shell: bash
         run: |
           curl -O --location https://elan.lean-lang.org/elan-init.sh
           sh elan-init.sh -y --default-toolchain stable
           rm elan-init.sh
 
       - name: modify PATH
-        shell: bash
         run: echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: check installation of elan
-        shell: bash
         run: elan --version
 
       - name: install latest stable version of Lean
-        shell: bash
         run: |
           elan toolchain install stable
 
       - name: check installation of Lean and lake
-        shell: bash
         run: |
           lean --version
           lake --version
 
   install_lean_for_mac:
     runs-on: macos-latest
+    defaults:
+      run:
+        shell: /bin/zsh {0}
     steps:
       - name: check dependencies
-        shell: zsh
         run: |
           git --version
           curl --version
 
       - name: install elan
-        shell: zsh
         run: |
           curl -O --location https://elan.lean-lang.org/elan-init.sh
           sh elan-init.sh -y --default-toolchain stable
           rm elan-init.sh
 
       - name: modify PATH
-        shell: zsh
         run: echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: check installation of elan
-        shell: zsh
         run: elan --version
 
       - name: install latest stable version of Lean
-        shell: zsh
         run: |
           elan toolchain install stable
 
       - name: check installation of Lean and lake
-        shell: zsh
         run: |
           lean --version
           lake --version

From 635c314860e0e26e37641893545414a66bcc37a1 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Fri, 29 May 2026 15:03:02 +0900
Subject: [PATCH 17/17] =?UTF-8?q?=E8=A8=98=E8=BF=B0=E3=81=AE=E4=BF=AE?=
 =?UTF-8?q?=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/HowToInstall.lean | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/LeanByExample/HowToInstall.lean b/LeanByExample/HowToInstall.lean
index 238f7e6a..21605522 100644
--- a/LeanByExample/HowToInstall.lean
+++ b/LeanByExample/HowToInstall.lean
@@ -137,19 +137,15 @@ lake --version
 
 ### git と curl のインストール
 
-MacOS の場合、`curl` は最初から入っていると思います。`git` が入っていない場合、次のコマンドでインストールできます。
-
-```zsh
-xcode-select --install
-```
-
-終わったら `git` と `curl` が使えるか確認します。
+まず `git` と `curl` が使えるか確認します。
 
 ```zsh
 git --version
 curl --version
 ```
 
+MacOS の場合、`curl` は最初から入っていると思います。`git` が入っていない場合でも、`git --version` の実行時にインストールするか聞かれるはずです。
+
 ### elan のインストール
 
 次に `elan` をインストールします。