diff --git a/TensorLib/Broadcast.lean b/TensorLib/Broadcast.lean
index 8bc5b7b..281c468 100644
--- a/TensorLib/Broadcast.lean
+++ b/TensorLib/Broadcast.lean
@@ -79,8 +79,8 @@ private theorem oneExtendPrefixLength (b : Broadcast) :
   rename_i left right
   simp [oneExtendPrefix]
   by_cases H : left.ndim <= right.ndim
-  . simp_all [Shape.ndim, H]
-  . simp_all [Shape.ndim, H]
+  . simp_all [Shape.ndim]
+  . simp_all [Shape.ndim]
     aesop (config := { warnOnNonterminal := false })
     rw [Nat.sub_add_cancel]
     omega
diff --git a/TensorLib/Slice.lean b/TensorLib/Slice.lean
index aa0ccb8..73da0aa 100644
--- a/TensorLib/Slice.lean
+++ b/TensorLib/Slice.lean
@@ -237,7 +237,7 @@ theorem stopRange (s : Slice) (dim : Nat) :
       by_cases H : k < -dim
       all_goals simp [H]
       by_cases H1 : k < 0
-      . simp [H, H1]
+      . simp [H1]
         aesop (config := { warnOnNonterminal := false })
         all_goals omega
       . aesop (config := { warnOnNonterminal := false })
diff --git a/lake-manifest.json b/lake-manifest.json
index 0dacfd0..0188d99 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,50 +5,50 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
+   "rev": "7d0e7a00681e1a0fc1ba732ac88055da2e0dd4f8",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
+   "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.22.0-rc4",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "TensorLib",
diff --git a/lakefile.lean b/lakefile.lean
index 09587b4..8a845f3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -28,13 +28,13 @@ lean_exe "tensorlib" where
   root := `Main
 
 require aesop from git
-  "https://github.com/leanprover-community/aesop" @ "v4.20.0"
+  "https://github.com/leanprover-community/aesop" @ "v4.22.0"
 
 require plausible from git
-  "https://github.com/leanprover-community/plausible" @ "v4.20.0"
+  "https://github.com/leanprover-community/plausible" @ "v4.22.0"
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli.git" @ "v4.20.0"
+  "https://github.com/leanprover/lean4-cli.git" @ "v4.22.0"
 
 require importGraph from git
-  "https://github.com/leanprover-community/import-graph.git" @ "v4.20.0"
+  "https://github.com/leanprover-community/import-graph.git" @ "v4.22.0"
diff --git a/lean-toolchain b/lean-toolchain
index 52fe774..6ac6d4c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.20.0
+leanprover/lean4:v4.22.0