diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean
index d556927af7a455..6ced6611a52bea 100644
--- a/Mathlib/Algebra/Exact.lean
+++ b/Mathlib/Algebra/Exact.lean
@@ -303,7 +303,7 @@ lemma of_ladder_linearEquiv_of_exact
 /-- Two maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P` are exact if and only if the induced maps
 `LinearMap.range f → N → LinearMap.range g` are exact. -/
 lemma iff_linearMap_rangeRestrict :
-    Exact f g ↔ Exact f.range.subtype g.rangeRestrict :=
+    Exact f g ↔ Exact (LinearMap.range f).subtype g.rangeRestrict :=
   iff_rangeFactorization (zero_mem (LinearMap.range g))
 
 alias ⟨linearMap_rangeRestrict, _⟩ := iff_linearMap_rangeRestrict
diff --git a/lake-manifest.json b/lake-manifest.json
index 7e802f8af4446e..2dee76ec2362e8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8cee626a680fe217814c4bd444b94ceb31efd6b6",
+   "rev": "77e08eddc486491d7b9e470926b3dbe50319451a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b",
+   "rev": "fa4f7f15d97591a9cf3aa7724ba371c7fc6dda02",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lakefile.lean b/lakefile.lean
index a156eb54eb1a5e..48d1ba8f9dbb2f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,7 +7,7 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "nightly-testing"
+require "leanprover-community" / "batteries" @ git "lean-pr-testing-8161"
 require "leanprover-community" / "Qq" @ git "master"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.56" -- ProofWidgets should always be pinned to a specific version
diff --git a/lean-toolchain b/lean-toolchain
index f9eeb051b72a0f..30999b3565f5a8 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-04-30
+leanprover/lean4:nightly-2025-05-01