Fixes for "chore: reimpement liftCoeM using Functor.map for a better defeq"

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 : α}
 

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

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-09-05
+leanprover/lean4-pr-releases:pr-release-10231-375347e