diff --git a/TensorLib/Broadcast.lean b/TensorLib/Broadcast.lean
index 281c468..e73aac6 100644
--- a/TensorLib/Broadcast.lean
+++ b/TensorLib/Broadcast.lean
@@ -81,8 +81,8 @@ private theorem oneExtendPrefixLength (b : Broadcast) :
   by_cases H : left.ndim <= right.ndim
   . simp_all [Shape.ndim]
   . simp_all [Shape.ndim]
-    aesop (config := { warnOnNonterminal := false })
-    rw [Nat.sub_add_cancel]
+    have hn : ¬ (left.val.length ≤ right.val.length) := by omega
+    simp only [hn, ↓reduceIte, List.length_append, List.length_replicate]
     omega
 
 private def matchPairs (b : Broadcast) : Option Shape :=
diff --git a/TensorLib/ByteArray.lean b/TensorLib/ByteArray.lean
index 0d9a4e1..483c3a3 100644
--- a/TensorLib/ByteArray.lean
+++ b/TensorLib/ByteArray.lean
@@ -155,7 +155,7 @@ private def roundTripUInt32BE (x : UInt32) : Bool := (toBEByteArray x).toUInt32B
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (x : UInt32) : roundTripUInt32LE x && roundTripUInt32BE x := by plausible
@@ -183,6 +183,7 @@ theorem _root_.ByteArray.replicateSize (n : Nat) : (ByteArray.replicate n v).siz
   rw [ByteArray.replicateSizeAux]
   unfold ByteArray.emptyWithCapacity ByteArray.size
   simp
+  rfl
 
 def _root_.ByteArray.zeros (n : Nat) : ByteArray := ByteArray.replicate n 0
 
@@ -247,7 +248,7 @@ private local instance : SampleableExt ByteArray :=
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (arr : ByteArray) :
@@ -258,7 +259,7 @@ example (arr : ByteArray) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (arr : ByteArray) :
diff --git a/TensorLib/Common.lean b/TensorLib/Common.lean
index 3258f98..89a478c 100644
--- a/TensorLib/Common.lean
+++ b/TensorLib/Common.lean
@@ -54,7 +54,7 @@ open Plausible
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (x y : Nat) :
@@ -71,7 +71,7 @@ local instance : SampleableExt (Nat × Nat) :=
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (xy : Nat × Nat) :
diff --git a/TensorLib/Dtype.lean b/TensorLib/Dtype.lean
index 7f2df3f..501edd8 100644
--- a/TensorLib/Dtype.lean
+++ b/TensorLib/Dtype.lean
@@ -1373,7 +1373,7 @@ private def canCastLosslessIntRoundTrip (fromDtype : Dtype) (n : Int) (toDtype :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (fromDtype toDtype : Dtype) (n : Nat) :
@@ -1384,7 +1384,7 @@ example (fromDtype toDtype : Dtype) (n : Nat) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 -- One dtype should always go back and forth
@@ -1395,7 +1395,7 @@ example (dtype : Dtype) (n : Nat) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 -- Lossless translations should be OK
@@ -1411,7 +1411,7 @@ example (fromDtype toDtype : Dtype) (n : Nat) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt16) :
@@ -1424,7 +1424,7 @@ example (a b : UInt16) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a : UInt16) :
@@ -1440,7 +1440,7 @@ example (a : UInt16) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt16) :
@@ -1452,7 +1452,7 @@ example (a b : UInt16) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt8) :
@@ -1464,7 +1464,7 @@ example (a b : UInt8) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt8) :
@@ -1478,7 +1478,7 @@ example (a b : UInt8) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : Dtype) : Dtype.join a b == Dtype.join b a := by plausible
diff --git a/TensorLib/Float.lean b/TensorLib/Float.lean
index 1bc96d8..82b5682 100644
--- a/TensorLib/Float.lean
+++ b/TensorLib/Float.lean
@@ -679,7 +679,7 @@ section Test
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
   #guard_msgs in
   example (bits : UInt16) :
@@ -719,7 +719,7 @@ warning: declaration uses 'sorry'
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
   example (bits : UInt16) :
@@ -777,7 +777,7 @@ warning: declaration uses 'sorry'
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
   example (bits : UInt8) :
@@ -790,7 +790,7 @@ warning: declaration uses 'sorry'
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
   example (bits : UInt8) :
diff --git a/TensorLib/Iterator.lean b/TensorLib/Iterator.lean
index 8dc9753..4ab06b7 100644
--- a/TensorLib/Iterator.lean
+++ b/TensorLib/Iterator.lean
@@ -37,7 +37,7 @@ namespace Iterator
 set_option synthInstance.checkSynthOrder false
 
 instance forInInstance [Monad m] [inst : Iterator iter value] : ForIn m iter value where
-  forIn {α} [Monad m] (iter : iter) (x : α) (f : value -> α -> m (ForInStep α)) : m α := do
+  forIn {α} (iter : iter) (x : α) (f : value -> α -> m (ForInStep α)) : m α := do
     let mut iter := iter
     let mut res := x
     for _ in [0:inst.size iter] do
diff --git a/TensorLib/Npy.lean b/TensorLib/Npy.lean
index 5c8f085..63c9275 100644
--- a/TensorLib/Npy.lean
+++ b/TensorLib/Npy.lean
@@ -125,7 +125,7 @@ def fromNpyString (s : String) : Err Dtype :=
   if s.length == 0 then .error "Empty dtype string" else
   do
     let order <- ByteOrder.fromChar (s.get 0)
-    let nameStr := s.drop 1
+    let nameStr := (s.drop 1).toString
     -- bf16 stored as "<V2" by ml_dtypes/JAX/TensorFlow (littleEndian)
     -- We only recognize "<V2" as bf16 to avoid collision with "|V2" (actual void data).
     -- Only littleEndian V2 is bf16. Tensor.toNpy always writes LE so this is safe.
diff --git a/lake-manifest.json b/lake-manifest.json
index d1ccc6a..e04c959 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,45 +1,46 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
+   "scope": "leanprover-community",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "TensorLib",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.lean b/lakefile.lean
index 00c4061..82b8de5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -28,10 +28,10 @@ lean_exe "tensorlib" where
   root := `Main
 
 require aesop from git
-  "https://github.com/leanprover-community/aesop" @ "v4.23.0"
+  "https://github.com/leanprover-community/aesop" @ "v4.33.0"
 
 require plausible from git
-  "https://github.com/leanprover-community/plausible" @ "v4.23.0"
+  "https://github.com/leanprover-community/plausible" @ "v4.33.0"
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli.git" @ "v4.23.0"
+  "https://github.com/leanprover/lean4-cli.git" @ "v4.33.0"
diff --git a/lean-toolchain b/lean-toolchain
index 7f254a9..a8afa7d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.23.0
+leanprover/lean4:v4.33.1