Lean と Mathlib のバージョン更新

Examples/Contents/InductionAp.lean

@@ -3,8 +3,7 @@
 
 `induction'` は `induction` の Lean 3 での構文を残したバージョンです．
 -/
-import Mathlib.Tactic.Ring
-import Mathlib.Tactic.Cases -- `induction'` のために必要
+import Mathlib.Tactic -- 大雑把に import する
 
 namespace InductionAp --#
 

Examples/Contents/Replace.lean

@@ -5,16 +5,14 @@
 `have` を使った場合，ローカルコンテキストにすでに `h : P` がある状態で，再び `h` という名前で別の命題を示すと，古い方の `h` はアクセス不能になって `†` が付いた状態になってしまいます．
 
 `replace` であれば，古い方が新しい方に置き換えられ，`†` の付いた命題は出現しません． -/
-import Mathlib.Algebra.Parity -- `Even` のために必要
-import Mathlib.Tactic.NthRewrite -- `nth_rw` のために必要
-import Mathlib.Tactic.Ring -- `ring` のために必要
+import Mathlib.Tactic -- 大雑把に import する
 
 /-- `5 * n` が偶数なら，`n` も偶数 -/
 example : ∀ (n : ℤ), Even (5 * n) → Even n := by
   intro n hn
 
   -- `Even (5 * n)` という仮定を分解
-  obtain ⟨ k, hk ⟩ := hn
+  obtain ⟨k, hk⟩ := hn
 
   -- 以下がローカルコンテキストに追加される
   guard_hyp hk : 5 * n = k + k

Examples/Contents/Rfl.lean

@@ -3,8 +3,7 @@
 `rfl` は，反射的(reflexive)な関係(relation)に対して関係式を示すタクティクです．ここで二項関係 `R : α → α → Prop` が反射的であるとは，任意の `a : α` に対して `R a a` が成り立つことをいいます．
 
 関係 `R` が反射的であることを `rfl` に利用させるには，`R` の反射性を示した定理に `@[refl]` タグを付けます．`@[refl]` で登録された定理を用いるので，追加でライブラリを import することにより示すことができる命題を増やせます． -/
-import Mathlib.Init.Data.Nat.Lemmas -- `n ≤ n` を示すために必要
-import Mathlib.Tactic.Relation.Rfl
+import Mathlib.Tactic -- 大雑把に import する
 
 universe u
 

Examples/Contents/Wlog.lean

@@ -1,8 +1,7 @@
 /- # wlog
 
 `wlog` は，数学でよく使われる，一般性を失うことなく(without loss of generarity)何々と仮定してよいというフレーズの Lean での対応物です． -/
-import Mathlib.Data.Int.Cast.Lemmas
-import Mathlib.Tactic.WLOG
+import Mathlib.Tactic -- 大雑把に import する
 
 -- `n` と `m` は自然数
 variable {n m : ℕ}

lake-manifest.json

@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06",
+   "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -31,7 +31,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236",
+   "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
+   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -67,10 +67,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "e091c88348ddd5acceddd4320811a926d4cf19d0",
+   "rev": "2b29e73438e240a427bcecc7c0fe19306beb1310",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0-rc2",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«Tactic Cheatsheet»",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.8.0