diff --git a/Solution/Advanced/Algebra/Lecture2.lean b/Solution/Advanced/Algebra/Lecture2.lean
index 4ce65f1..22be2fa 100644
--- a/Solution/Advanced/Algebra/Lecture2.lean
+++ b/Solution/Advanced/Algebra/Lecture2.lean
@@ -31,7 +31,7 @@ variable [Group G₁] [Group G₂] {f : G₁ →* G₂}
 -- `f`と`a : G₁`に対して、いちいち`f.toFun a`と書く代わりに、`f a`と書くためのおまじない
 -- （`f`そのものは、写像`f.toFun`と、それが積を保つという事実`f.map_mul'`を束ねたもので、本来は写像でない）
 -- 右側のInfoviewには、`f a`の代わりに`↑f a`と表示されることもあるが、同じなので気にしないでください。
-instance : FunLike (G₁ →* G₂) G₁ (fun _ ↦ G₂) where
+instance : DFunLike (G₁ →* G₂) G₁ (fun _ ↦ G₂) where
   coe := fun f ↦ f.toFun
   coe_injective' f₁ f₂ _ := by cases f₁; cases f₂; congr
 
diff --git a/Solution/Advanced/Algebra/Lecture3.lean b/Solution/Advanced/Algebra/Lecture3.lean
index 7f91fb6..2c5cc73 100644
--- a/Solution/Advanced/Algebra/Lecture3.lean
+++ b/Solution/Advanced/Algebra/Lecture3.lean
@@ -148,7 +148,7 @@ notation:25 X " →[" G:25 "] " Y:0 => GroupActionHom G X Y
 variable [Group G] [GroupAction G X] [GroupAction G Y] [GroupAction G Z]
 
 -- `f : X →[G] Y`に対して`f x`のように書くためのおまじない。
-instance : FunLike (GroupActionHom G X Y) X (fun _ ↦ Y) where
+instance : DFunLike (GroupActionHom G X Y) X (fun _ ↦ Y) where
   coe f := f.toFun
   coe_injective' f₁ f₂ _ := by cases f₁; cases f₂; congr
 
@@ -161,7 +161,7 @@ theorem GroupActionHom.coe_coe (f : X → Y) (h) : ((⟨f, h⟩ : X →[G] Y) :
 -- 定義からすぐ分かること
 @[ext]
 theorem GroupActionHom.ext {f₁ f₂ : X →[G] Y} : (∀ x, f₁ x = f₂ x) → f₁ = f₂ :=
-  FunLike.ext f₁ f₂
+  DFunLike.ext f₁ f₂
 
 theorem map_smul (f : X →[G] Y) : ∀ (a : G) (x : X), f (a • x) = a • f x := f.map_smul'
 
diff --git a/Solution/Advanced/Category/Lecture1.lean b/Solution/Advanced/Category/Lecture1.lean
index abeb828..85f5671 100644
--- a/Solution/Advanced/Category/Lecture1.lean
+++ b/Solution/Advanced/Category/Lecture1.lean
@@ -175,6 +175,8 @@ instance {R : CommRingCat} : Category (CommAlgCat R) where
 /- 定義の上の`@[simps]`はおまじないで、ここでは特に意味がない。`Lecture 2`で役に立つ。 -/
 
 -- おまじない。`Lecture 2`で役に立つ。
+instance {A B : CommAlgCat R} : FunLike (Hom A B) A B :=
+  inferInstanceAs <| FunLike (A →ₐ[R] B) A B
 instance {A B : CommAlgCat R} : AlgHomClass (Hom A B) R A B :=
   inferInstanceAs <| AlgHomClass (A →ₐ[R] B) R A B
 
diff --git a/lake-manifest.json b/lake-manifest.json
index d8ca4a8..bc9e5f6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,28 +1,28 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Seasawher/mk-exercise",
+ [{"url": "https://github.com/Seasawher/mk-exercise.git",
    "type": "git",
    "subDir": null,
    "rev": "70102f2963f5bc19aac0339d9464b72a1de2e1cb",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "70102f2963f5bc19aac0339d9464b72a1de2e1cb",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0f6bc5b32bf5b0498902d3b5f0806c75530539d5",
+   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,19 +31,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.29",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,13 +55,22 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "afe6b29fd5ae8baf11db1d2c2921b9730d9f7ad0",
+   "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "afe6b29fd5ae8baf11db1d2c2921b9730d9f7ad0",
+   "inputRev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«lean-math-workshop»",
diff --git a/lakefile.lean b/lakefile.lean
index 4011b70..ec2c7c5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -14,7 +14,7 @@ require «mk-exercise» from git
   "https://github.com/Seasawher/mk-exercise.git" @ "70102f2963f5bc19aac0339d9464b72a1de2e1cb"
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "afe6b29fd5ae8baf11db1d2c2921b9730d9f7ad0"
+  "https://github.com/leanprover-community/mathlib4.git" @ "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb"
 
 @[default_target]
 lean_lib «Solution» where
diff --git a/lean-toolchain b/lean-toolchain
index 3f21e50..5026204 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.6.0