diff --git a/Examples/Command/Declarative/DeclareSyntaxCat.lean b/Examples/Command/Declarative/DeclareSyntaxCat.lean
index dff49152..dbaccb96 100644
--- a/Examples/Command/Declarative/DeclareSyntaxCat.lean
+++ b/Examples/Command/Declarative/DeclareSyntaxCat.lean
@@ -14,7 +14,7 @@ def Set (α : Type u) := α → Prop
 variable {α : Type u}
 
 /-- 項 `x : α` が `X : Set α` に属する -/
-def Set.mem (x : α) (X : Set α) : Prop := X x
+def Set.mem (X : Set α) (x : α) : Prop := X x
 
 /-- `x ∈ X` と書けるようにする -/
 instance : Membership α (Set α) where
diff --git a/Examples/Command/Diagnostic/Time.lean b/Examples/Command/Diagnostic/Time.lean
index 26203216..85a6124f 100644
--- a/Examples/Command/Diagnostic/Time.lean
+++ b/Examples/Command/Diagnostic/Time.lean
@@ -1,7 +1,7 @@
 /- # \#time
 `#time` は、コマンドの実行時間を計測するためのコマンドです。ミリ秒単位で結果を出してくれます。
 -/
-import Mathlib.Util.Time
+import Lean
 namespace Time --#
 
 -- フィボナッチ数列の遅い実装
diff --git a/Examples/Solution/CantorTheorem.lean b/Examples/Solution/CantorTheorem.lean
index 5d7f28e6..0b026dea 100644
--- a/Examples/Solution/CantorTheorem.lean
+++ b/Examples/Solution/CantorTheorem.lean
@@ -39,7 +39,7 @@ def Set (α : Type) := α → Prop
 variable {α : Type}
 
 /-- `a : α` は集合 `s` に属する。数学では普通 `a ∈ s` と書かれる。 -/
-def Set.mem (a : α) (s : Set α) : Prop := s a
+def Set.mem (s : Set α) (a : α) : Prop := s a
 
 /-- `s a` を `a ∈ s` と書けるようにする。 -/
 instance : Membership α (Set α) := ⟨Set.mem⟩
diff --git a/Examples/Tactic/AcRfl.lean b/Examples/Tactic/AcRfl.lean
index 2fb704b2..be84a15c 100644
--- a/Examples/Tactic/AcRfl.lean
+++ b/Examples/Tactic/AcRfl.lean
@@ -107,7 +107,7 @@ protected theorem add_assoc (a b c : Color) : a + b + c = a + (b + c) := by
 -- Commutative のインスタンスはないことが確認できる
 /--
 error: failed to synthesize
-  Std.Commutative fun x x_1 => x + x_1
+  Std.Commutative fun x1 x2 => x1 + x2
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/Examples/Tactic/Linarith.lean b/Examples/Tactic/Linarith.lean
index b03313f7..2f8a78d8 100644
--- a/Examples/Tactic/Linarith.lean
+++ b/Examples/Tactic/Linarith.lean
@@ -2,7 +2,6 @@
 
 `linarith` は線形算術(linear arithmetic)を行うタクティクです。Fourier-Motzkin elimination を用いて、線形な(不)等式系から矛盾を導こうとします。一般に、ゴールが `False` でないときにはゴールの否定を仮定に加えることで、ゴールを閉じようとします。 -/
 import Mathlib.Tactic.Linarith -- `linarith` のために必要
-import Mathlib.Util.Time -- `#time` を使うため --#
 import Batteries.Data.Rat.Basic -- `ℚ` のために必要
 
 variable (x y z : ℚ)
diff --git a/Exercise/CantorTheorem.lean b/Exercise/CantorTheorem.lean
index 048c4130..835ed85f 100644
--- a/Exercise/CantorTheorem.lean
+++ b/Exercise/CantorTheorem.lean
@@ -39,7 +39,7 @@ def Set (α : Type) := α → Prop
 variable {α : Type}
 
 /-- `a : α` は集合 `s` に属する。数学では普通 `a ∈ s` と書かれる。 -/
-def Set.mem (a : α) (s : Set α) : Prop := s a
+def Set.mem (s : Set α) (a : α) : Prop := s a
 
 /-- `s a` を `a ∈ s` と書けるようにする。 -/
 instance : Membership α (Set α) := ⟨Set.mem⟩
diff --git a/lake-manifest.json b/lake-manifest.json
index cc0d6d50..3a84a61c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,21 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Seasawher/mk-exercise.git",
+ [{"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a8526d4747854dcbef1c552b3031d17e5a956c0",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/Seasawher/mk-exercise.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7d99b9c7ce00ad4c59bb06060e1a19b2e1cc7f57",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bdfc2e355fbd5003be7094b3c99ff9d833aff7da",
+   "rev": "b6ca4bba32cdfa94c98bd8598397d9c3888d68c0",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -45,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
+   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,27 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0194b29f8e8bda212a44bbd34bf8b8c37a88db25",
+   "rev": "19b4c40bc454221b94bcaeb093d849639273e6cc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lean-toolchain b/lean-toolchain
index 5a9c76dc..98556ba0 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0-rc1