diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean
index 045581a..368ee1b 100644
--- a/DocGen4/Hierarchy.lean
+++ b/DocGen4/Hierarchy.lean
@@ -11,9 +11,8 @@ namespace DocGen4
 open Lean Std Name
 
 def getNLevels (name : Name) (levels: Nat) : Name :=
-    (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
-  where
-    components := name.components'
+  let components := name.components'
+  (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
 
 inductive Hierarchy where
 | node (name : Name) (isFile : Bool) (children : RBNode Name (λ _ => Hierarchy)) : Hierarchy
@@ -54,8 +53,6 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do
   let hn := h.getName
   let mut cs := h.getChildren
 
-  assert! getNumParts hn ≤ getNumParts n
-
   if getNumParts hn + 1 == getNumParts n then
     match cs.find Name.cmp n with
     | none =>
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index c369cc1..48e86ad 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -38,14 +38,12 @@ def moduleNameToLink (n : Name) : HtmlM String := do
   (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
 def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
-    FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
-  where
-    parts := n.components.map Name.toString
+  let parts := n.components.map Name.toString
+  FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
 
 def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
-    basePath / parts.foldl (· / ·) (FilePath.mk ".")
-  where
-    parts := n.components.dropLast.map Name.toString
+  let parts := n.components.dropLast.map Name.toString
+  basePath / parts.foldl (· / ·) (FilePath.mk ".")
 
 section Static
   def styleCss : String := include_str "./static/style.css"
diff --git a/lean-toolchain b/lean-toolchain
index 6386ac4..ff3b224 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-01-04
+leanprover/lean4:nightly-2022-01-15