diff --git a/lake-manifest.json b/lake-manifest.json
index caf5715..4ab7a72 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,22 +1,24 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Seasawher/mdgen",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
-   "name": "mdgen",
+   "scope": "leanprover-community",
+   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v1.3.0",
+   "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/std4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "scope": "",
+   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
+   "name": "mdgen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v1.3.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«lean4-metaprogramming-book»",
diff --git a/lakefile.lean b/lakefile.lean
index c84ca45..f45d0b1 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,7 +12,7 @@ lean_lib «lean4-metaprogramming-book» where
 require mdgen from git
   "https://github.com/Seasawher/mdgen" @ "v1.3.0"
 
-require std from git "https://github.com/leanprover/std4" @ "v4.7.0"
+require "leanprover-community" / "batteries" @ git "main"
 
 def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   let out ← IO.Process.output {
diff --git a/lean-toolchain b/lean-toolchain
index 9ad3040..3450f2d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.15.0-rc1
\ No newline at end of file
diff --git a/lean/main/01_intro.lean b/lean/main/01_intro.lean
index 3401465..7fd6d8e 100644
--- a/lean/main/01_intro.lean
+++ b/lean/main/01_intro.lean
@@ -130,10 +130,17 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
 
 /-- info: success -/
 #guard_msgs in --#
-#assertType 5  : Nat
-
-/-- error: failure -/
-#guard_msgs in --#
+#assertType 5 : Nat
+
+/--
+error: type mismatch
+  []
+has type
+  List ?m.3211 : Type ?u.3210
+but is expected to have type
+  Nat : Type
+-/
+#guard_msgs (error) in --#
 #assertType [] : Nat
 
 /-! We started by using `elab` to define a `command` syntax. When parsed
diff --git a/lean/main/05_syntax.lean b/lean/main/05_syntax.lean
index b091548..2828933 100644
--- a/lean/main/05_syntax.lean
+++ b/lean/main/05_syntax.lean
@@ -508,7 +508,7 @@ Let's define a simple theory of sets to test it:
 -- -> a simple predicate on the type of its elements
 def Set (α : Type u) := α → Prop
 
-def Set.mem (x : α) (X : Set α) : Prop := X x
+def Set.mem (X : Set α) (x : α) : Prop := X x
 
 -- Integrate into the already existing typeclass for membership notation
 instance : Membership α (Set α) where
@@ -619,14 +619,14 @@ the bound variables, we refer the reader to the macro chapter.
     Use the following template:
 
     ```lean
-    import Std.Classes.SetNotation
-    import Std.Util.ExtendedBinder
+    import Batteries.Classes.SetNotation
+    import Batteries.Util.ExtendedBinder
     syntax (name := bigsumin) ...
     -- our "elaboration function" that infuses syntax with semantics
     @[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
     ```
 
-    Hint: use the `Std.ExtendedBinder.extBinder` parser.
-    Hint: you need Std4 installed in your Lean project for these imports to work.
+    Hint: use the `Batteries.ExtendedBinder.extBinder` parser.
+    Hint: you need Batteries installed in your Lean project for these imports to work.
 
 -/
diff --git a/lean/main/06_macros.lean b/lean/main/06_macros.lean
index e42be4b..c3323fa 100644
--- a/lean/main/06_macros.lean
+++ b/lean/main/06_macros.lean
@@ -454,7 +454,7 @@ As promised in the syntax chapter here is Binders 2.0. We'll start by
 reintroducing our theory of sets:
 -/
 def Set (α : Type u) := α → Prop
-def Set.mem (x : α) (X : Set α) : Prop := X x
+def Set.mem (X : Set α) (x : α) : Prop := X x
 
 -- Integrate into the already existing typeclass for membership notation
 instance : Membership α (Set α) where
diff --git a/lean/main/07_elaboration.lean b/lean/main/07_elaboration.lean
index ac904c9..e29316e 100644
--- a/lean/main/07_elaboration.lean
+++ b/lean/main/07_elaboration.lean
@@ -274,21 +274,21 @@ Adding new term elaborators works basically the same way as adding new
 command elaborators so we'll only take a very brief look:
 -/
 
-syntax (name := myterm1) "myterm 1" : term
+syntax (name := myterm1) "myterm_1" : term
 
 def mytermValues := [1, 2]
 
 @[term_elab myterm1]
-def myTerm1Impl : TermElab := fun stx type? =>
+def myTerm1Impl : TermElab := fun stx type? => do
   mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 0] -- `MetaM` code
 
-#eval myterm 1 -- 1
+#eval myterm_1 -- 1
 
 -- Also works with `elab`
-elab "myterm 2" : term => do
+elab "myterm_2" : term => do
   mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 1] -- `MetaM` code
 
-#eval myterm 2 -- 2
+#eval myterm_2 -- 2
 
 /-!
 ### Mini project
diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean
index a02134b..5cd7a1a 100644
--- a/lean/main/09_tactics.lean
+++ b/lean/main/09_tactics.lean
@@ -386,7 +386,7 @@ elab "custom_assump_2" : tactic =>
         then return Option.some declExpr
         else return Option.none
     match option_matching_expr with
-    | some e => Lean.Elab.Tactic.closeMainGoal e
+    | some e => Lean.Elab.Tactic.closeMainGoal `custom_assump_2 e
     | none =>
       Lean.Meta.throwTacticEx `custom_assump_2 goal
         (m!"unable to find matching hypothesis of type ({goalType})")
diff --git a/lean/solutions/05_syntax.lean b/lean/solutions/05_syntax.lean
index 76dea63..2c5cba2 100644
--- a/lean/solutions/05_syntax.lean
+++ b/lean/solutions/05_syntax.lean
@@ -1,6 +1,6 @@
 import Lean
 import Lean.Parser.Syntax
-import Std.Util.ExtendedBinder
+import Batteries.Util.ExtendedBinder
 
 open Lean Elab Command Term
 
@@ -28,7 +28,7 @@ open a
 
 /- ### 2. -/
 
-syntax "good morning" : term
+syntax "good" "morning" : term
 syntax "hello" : command
 syntax "yellow" : tactic
 
@@ -70,8 +70,8 @@ def elabHelp : CommandElab := fun stx => Lean.logInfo "success!"
 
 /- ### 5. -/
 
--- Note: std4 has to be in dependencies of your project for this to work.
-syntax (name := bigsumin) "∑ " Std.ExtendedBinder.extBinder "in " term "," term : term
+-- Note: Batteries has to be in dependencies of your project for this to work.
+syntax (name := bigsumin) "∑ " Batteries.ExtendedBinder.extBinder "in " term "," term : term
 
 @[term_elab bigsumin]
 def elabSum : TermElab := fun stx tp =>
diff --git a/lean/solutions/09_tactics.lean b/lean/solutions/09_tactics.lean
index 145080e..9a7a921 100644
--- a/lean/solutions/09_tactics.lean
+++ b/lean/solutions/09_tactics.lean
@@ -10,8 +10,8 @@ elab "step_1" : tactic => do
   let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"
 
   -- 1. Create new `_`s with appropriate types.
-  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
-  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := `red)
+  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := `blue)
 
   -- 2. Assign the main goal to the expression `Iff.intro _ _`.
   mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
@@ -60,8 +60,8 @@ elab "step_3" : tactic => do
   let Expr.app (Expr.app (Expr.const `And _) q) p := goalType | throwError "Goal type is not of the form `And q p`"
 
   -- 1. Create new `_`s with appropriate types.
-  let mvarId1 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances q (userName := "red1")
-  let mvarId2 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances p (userName := "red2")
+  let mvarId1 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances q (userName := `red1)
+  let mvarId2 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances p (userName := `red2)
 
   -- 2. Assign the main goal to the expression `And.intro _ _`.
   mvarId.assign (← mkAppM `And.intro #[mvarId1, mvarId2])
@@ -109,8 +109,8 @@ elab "forker_a" : tactic => do
   liftMetaTactic fun mvarId => do
     let (Expr.app (Expr.app (Expr.const `And _) p) q) ← mvarId.getType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
 
-    let mvarIdP ← mkFreshExprMVar p (userName := "red")
-    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+    let mvarIdP ← mkFreshExprMVar p (userName := `red)
+    let mvarIdQ ← mkFreshExprMVar q (userName := `blue)
 
     let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
     mvarId.assign proofTerm
@@ -124,8 +124,8 @@ elab "forker_b" : tactic => do
   let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
 
   mvarId.withContext do
-    let mvarIdP ← mkFreshExprMVar p (userName := "red")
-    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+    let mvarIdP ← mkFreshExprMVar p (userName := `red)
+    let mvarIdQ ← mkFreshExprMVar q (userName := `blue)
 
     let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
     mvarId.assign proofTerm
@@ -139,8 +139,8 @@ elab "forker_c" : tactic => do
   let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
 
   mvarId.withContext do
-    let mvarIdP ← mkFreshExprMVar p (userName := "red")
-    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+    let mvarIdP ← mkFreshExprMVar p (userName := `red)
+    let mvarIdQ ← mkFreshExprMVar q (userName := `blue)
 
     let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
     mvarId.assign proofTerm