diff --git a/Solution/Advanced/Category/Lecture2.lean b/Solution/Advanced/Category/Lecture2.lean
index c53e5dd..5a3b9b0 100644
--- a/Solution/Advanced/Category/Lecture2.lean
+++ b/Solution/Advanced/Category/Lecture2.lean
@@ -1,5 +1,5 @@
 import Solution.Advanced.Category.Lecture1
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 namespace Tutorial
 
diff --git a/Solution/Basic/Lecture1.lean b/Solution/Basic/Lecture1.lean
index cd97e05..455f6c5 100644
--- a/Solution/Basic/Lecture1.lean
+++ b/Solution/Basic/Lecture1.lean
@@ -8,7 +8,7 @@ example : 1 + 1 = 2 := by
 
 -- 正しい証明に書き直そう！
 example : 1 + 1 = 2 := by
-  triv
+  trivial
 
 /- # Leanにおける論理
 数学的に意味のある文を**命題**と呼ぶ。例えば、「1 + 1 = 2」「3は偶数である」「リーマン予想」などが
diff --git a/lake-manifest.json b/lake-manifest.json
index bc9e5f6..f06cf96 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -13,16 +13,16 @@
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +31,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.29",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "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": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "rev": "a45ae63747140c1b2cbad9d46f518015c047047a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«lean-math-workshop»",
diff --git a/lakefile.lean b/lakefile.lean
index ec2c7c5..d45f79e 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" @ "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.7.0"
 
 @[default_target]
 lean_lib «Solution» where
diff --git a/lean-toolchain b/lean-toolchain
index 5026204..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0