diff --git a/LSpec/Instances.lean b/LSpec/Instances.lean
index 94ee15c..c1c6398 100644
--- a/LSpec/Instances.lean
+++ b/LSpec/Instances.lean
@@ -56,7 +56,7 @@ instance Nat.Testable_forall_lt
           | none     => s!"Fails on input {b}."
       | .isFailure msg => .isFailure msg
     | .isMaybe msg => .isMaybe msg
-    | .isFalse h msg => .isFalse (λ h' => h λ n hn => h' _ (Nat.le_step hn)) msg
+    | .isFalse h msg => .isFalse (λ h' => h λ n hn => h' _ (Nat.le_succ_of_le hn)) msg
     | .isFailure msg => .isFailure msg
 
 end LSpec
diff --git a/LSpec/LSpec.lean b/LSpec/LSpec.lean
index 3dab516..a425c13 100644
--- a/LSpec/LSpec.lean
+++ b/LSpec/LSpec.lean
@@ -129,7 +129,7 @@ def withExceptError (descr : String) (exc : Except ε α) [ToString α]
 
 /-- A generic runner for `TestSeq` -/
 def TestSeq.run (tSeq : TestSeq) (indent := 0) : Bool × String :=
-  let pad := String.mk $ List.replicate indent ' '
+  let pad := String.ofList $ List.replicate indent ' '
   let rec aux (acc : String) : TestSeq → Bool × String
     | .done => (true, acc)
     | .group d ts n =>
diff --git a/flake.lock b/flake.lock
index 0a5c5f4..ad7a75d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1761368467,
-        "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=",
+        "lastModified": 1765913099,
+        "narHash": "sha256-81IuI/Q/y9QG5gLK4ZKzlHC+mVb2SvbyS71Ro2FmOK8=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "3550873ed1a87d666d633d34921e79abaa4671c1",
+        "rev": "ee3a6aeb480713b2e69618117d0e0ff5562091d1",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 69795e7..a947657 100644
--- a/flake.nix
+++ b/flake.nix
@@ -27,7 +27,8 @@
         self',
         config,
         ...
-      }: {
+      }: let lake2nix = pkgs.callPackage lean4-nix.lake {};
+        in {
         _module.args.pkgs = import nixpkgs {
           inherit system;
           overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
@@ -35,10 +36,10 @@
 
         # Build the library with `nix build`
         packages.default =
-          ((lean4-nix.lake {inherit pkgs;}).mkPackage {
+          lake2nix.mkPackage {
+            name = "LSpec";
             src = ./.;
-            roots = ["LSpec"];
-          }).modRoot;
+          };
 
         devShells.default = pkgs.mkShell {
           packages = with pkgs.lean; [lean-all];
diff --git a/lean-toolchain b/lean-toolchain
index c00a535..e59446d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.26.0