diff --git a/LeanByExample/Reference/Tactic/Trans.lean b/LeanByExample/Reference/Tactic/Trans.lean
index ad0c914..a61b11a 100644
--- a/LeanByExample/Reference/Tactic/Trans.lean
+++ b/LeanByExample/Reference/Tactic/Trans.lean
@@ -4,7 +4,7 @@
 
 推移的な関係 `∼` に対してゴールが `a ∼ c` であるとき、`trans b` により2つのサブゴール `a ∼ b` と `b ∼ c` が生成されます。[`calc`](./Calc.md) を使っても同じことができますが、`calc` を使うまでもないときに便利かもしれません。
 -/
-import Mathlib.Tactic.Relation.Trans
+import Batteries.Tactic.Trans
 
 example {n m : Nat} (h1 : n ≤ 1) (h2 : 1 ≤ m) : n ≤ m := by
   -- 1 を仲介して示す
diff --git a/lake-manifest.json b/lake-manifest.json
index e22231f..3577234 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e998043adeebf96ab1c66d4f47eaea68c824f9cb",
+   "rev": "14d53f0bfb9b18d8555b82deaad3706fda61d05d",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1e0bf50b357069e1d658512a579a5faac6587c40",
+   "rev": "dd6b1019b5cef990161bf3edfebeb6b0be78044a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "418a5eb7aec3fb639097cb13f74fc031ac4057f2",
+   "rev": "5958e95eebccc498ea68b5a74d00bd9d2ce5804c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",