From 68f0918121241ab1b090ef8782e806e99479e984 Mon Sep 17 00:00:00 2001
From: leanprover-community-mathlib4-bot
 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Date: Sat, 6 Sep 2025 13:15:34 +0000
Subject: [PATCH 1/2] Update lean-toolchain for testing
 https://github.com/leanprover/lean4/pull/10231

---
 lake-manifest.json | 4 ++--
 lakefile.lean      | 2 +-
 lean-toolchain     | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 2887d845647542..698b7710ae0df6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0199022f5d514ee76dcc5b0ebc0aa9ca37112930",
+   "rev": "77307c872d0de07dba55c6029f003207130b8ca4",
    "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 d281291b1f8344..8ada503da97e10 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,7 +6,7 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ 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.71" -- ProofWidgets should always be pinned to a specific version
diff --git a/lean-toolchain b/lean-toolchain
index da4c44b000f4cb..c68632e0eb6e63 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-09-05
+leanprover/lean4-pr-releases:pr-release-10231-375347e

From 5356dfa7560169ea7f1f54468cbd6ac4944dc178 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 8 Sep 2025 22:54:54 +0000
Subject: [PATCH 2/2] fix

---
 Mathlib/Data/Set/Functor.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Data/Set/Functor.lean b/Mathlib/Data/Set/Functor.lean
index 3d8f53bc61bf75..b930d301b57ca8 100644
--- a/Mathlib/Data/Set/Functor.lean
+++ b/Mathlib/Data/Set/Functor.lean
@@ -81,13 +81,13 @@ instance : Alternative Set :=
 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
@@ -104,11 +104,8 @@ In practice this is only used for applying the `Set` functor to `Subtype.val`,
 as was defined in `Data.Set.Notation`. -/
 
 /-- 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 α _ Set.monad t = (t : Set α) := 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 : α}