sync ワークフローの修正とテスト実行

.github/workflows/sync.yml

@@ -36,6 +36,8 @@ jobs:
     steps:
       - name: checkout
         uses: actions/checkout@v4
+        with:
+          ref: ${{ github.event.pull_request.head.ref }}
 
       - name: Install elan
         run: |
@@ -63,4 +65,4 @@ jobs:
           git config user.email "[email protected]"
           git add Examples/Exercise
           git commit -m "generated by GitHub Action"
-          git push
+          git push origin HEAD:${{ github.event.pull_request.head.ref }}

Examples/Exercise/CantorTheorem.lean

@@ -13,7 +13,9 @@ Cantor の定理とは、次のような定理です。
 ということを意味しています。
 ```
 
-この定理はもちろん Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。
+「濃度」とは、集合の「要素の個数」という概念を無限集合にも拡張したものであり、おおむね「一対一で漏れのない対応がつけられるならば、要素数が等しいと言ってよいだろう」というアイデアに基づくものです。
+
+この Cantor の定理はよく知られたものであり、Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。
 -/
 
 /- ## 集合論の形式化

Examples/Solution/CantorTheorem.lean

@@ -13,7 +13,9 @@ Cantor の定理とは、次のような定理です。
 ということを意味しています。
 ```
 
-この定理はもちろん Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。
+「濃度」とは、集合の「要素の個数」という概念を無限集合にも拡張したものであり、おおむね「一対一で漏れのない対応がつけられるならば、要素数が等しいと言ってよいだろう」というアイデアに基づくものです。
+
+この Cantor の定理はよく知られたものであり、Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。
 -/
 
 /- ## 集合論の形式化