chore: adaptations for nightly-2025-05-01

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

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",

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-04-30
+leanprover/lean4:nightly-2025-05-01