diff --git a/Mathlib/Data/Set/Functor.lean b/Mathlib/Data/Set/Functor.lean
index 3e4f963de5d8ac..152ea050812984 100644
--- a/Mathlib/Data/Set/Functor.lean
+++ b/Mathlib/Data/Set/Functor.lean
@@ -118,13 +118,13 @@ instance : LawfulMonad Set where
 variable {β : Set α} {γ : Set β}
 
 theorem mem_coe_of_mem {a : α} (ha : a ∈ β) (ha' : ⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α) :=
-  ⟨_, ⟨⟨_, rfl⟩, _, ⟨ha', rfl⟩, rfl⟩⟩
+  ⟨⟨a, ha⟩, ha', rfl⟩
 
 theorem coe_subset : (γ : Set α) ⊆ β := by
-  intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩; convert ha
+  rintro _ ⟨⟨b, hb⟩, ha, rfl⟩; exact hb
 
 theorem mem_of_mem_coe {a : α} (ha : a ∈ (γ : Set α)) : ⟨a, coe_subset ha⟩ ∈ γ := by
-  rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩; convert ha
+  rcases ha with ⟨⟨b, hb⟩, hb', rfl⟩; convert hb'
 
 theorem eq_univ_of_coe_eq (hγ : (γ : Set α) = β) : γ = univ :=
   eq_univ_of_forall fun ⟨_, ha⟩ => mem_of_mem_coe <| hγ.symm ▸ ha
@@ -142,11 +142,8 @@ as was defined in `Data.Set.Notation`. -/
 
 attribute [local instance] Set.monad in
 /-- The coercion from `Set.monad` as an instance is equal to the coercion in `Data.Set.Notation`. -/
-theorem coe_eq_image_val (t : Set s) :
-    @Lean.Internal.coeM Set s α _ _ t = Subtype.val '' t := by
-  change ⋃ (x ∈ t), {x.1} = _
-  ext
-  simp
+@[simp] theorem coe_eq_image_val (t : Set s) :
+    @Lean.Internal.coeM Set s α _ Set.monad t = Subtype.val '' t := rfl
 
 variable {β : Set α} {γ : Set β} {a : α}
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 5256913d9e3b9c..d5e2abfab299de 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9eab46cb0b18faa48a241f2e03f7304d4e19ebe0",
+   "rev": "5cb2df43d82495e4d0ec1327979545427b57e53c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-10231",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index af04c3360e4dd6..b148248ee10d32 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,8 +6,8 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "nightly-testing"
-require "leanprover-community" / "Qq" @ git "nightly-testing"
+require "leanprover-community" / "batteries" @ git "lean-pr-testing-10231"
+require "leanprover-community" / "Qq" @ git "master"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.83-pre2" -- ProofWidgets should always be pinned to a specific version
   with NameMap.empty.insert `errorOnBuild
diff --git a/lean-toolchain b/lean-toolchain
index c2d2f902334cda..2cad1c346ddcf9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-01
+leanprover/lean4-pr-releases:pr-release-10231-08ee111