diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
index d63c9affb02162..b618cae5ddbdad 100644
--- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
+++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
@@ -439,14 +439,12 @@ noncomputable instance : Category (Localization W) where
   comp_id := by
     rintro (X Y : C) f
     obtain ⟨z, rfl⟩ := Hom.mk_surjective f
-    change (Hom.mk z).comp (Hom.mk (ofHom W (𝟙 Y))) = Hom.mk z
     rw [Hom.comp_eq, comp_eq z (ofHom W (𝟙 Y)) (ofInv z.s z.hs) (by simp)]
     dsimp [comp₀]
     simp only [comp_id, id_comp]
   id_comp := by
     rintro (X Y : C) f
     obtain ⟨z, rfl⟩ := Hom.mk_surjective f
-    change (Hom.mk (ofHom W (𝟙 X))).comp (Hom.mk z) = Hom.mk z
     rw [Hom.comp_eq, comp_eq (ofHom W (𝟙 X)) z (ofHom W z.f) (by simp)]
     dsimp
     simp only [id_comp, comp_id]
@@ -455,8 +453,6 @@ noncomputable instance : Category (Localization W) where
     obtain ⟨z₁, rfl⟩ := Hom.mk_surjective f₁
     obtain ⟨z₂, rfl⟩ := Hom.mk_surjective f₂
     obtain ⟨z₃, rfl⟩ := Hom.mk_surjective f₃
-    change ((Hom.mk z₁).comp (Hom.mk z₂)).comp (Hom.mk z₃) =
-      (Hom.mk z₁).comp ((Hom.mk z₂).comp (Hom.mk z₃))
     rw [Hom.comp_eq z₁ z₂, Hom.comp_eq z₂ z₃]
     obtain ⟨z₁₂, fac₁₂⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs z₂.f)
     obtain ⟨z₂₃, fac₂₃⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs z₃.f)
diff --git a/Mathlib/Combinatorics/Matroid/Rank/Cardinal.lean b/Mathlib/Combinatorics/Matroid/Rank/Cardinal.lean
index ed16471e093a17..3d27b1da30689b 100644
--- a/Mathlib/Combinatorics/Matroid/Rank/Cardinal.lean
+++ b/Mathlib/Combinatorics/Matroid/Rank/Cardinal.lean
@@ -151,7 +151,7 @@ theorem Indep.cRk_eq_cardinalMk (hI : M.Indep I) : #I = M.cRk I :=
     (hX : X ⊆ M.E := by aesop_mat) : lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift (M.cRk X) := by
   nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup (bddAbove_range _), cRk, cRank, cRk, cRank]
   nth_rw 2 [lift_iSup (bddAbove_range _)]
-  simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, isBase_restrict_iff',
+  simp only [ciSup_le_iff (bddAbove_range _), Subtype.forall, isBase_restrict_iff',
     isBasis'_iff_isBasis hX, isBasis'_iff_isBasis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
   refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩
   · obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_isBasis_iff'.1 hI
@@ -174,7 +174,7 @@ theorem cRk_map_eq {β : Type u} {f : α → β} {X : Set β} (M : Matroid α) (
     lift.{v, u} ((M.comap f).cRk X) = lift (M.cRk (f '' X)) := by
   nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup (bddAbove_range _), cRk, cRank, cRk, cRank]
   nth_rw 2 [lift_iSup (bddAbove_range _)]
-  simp only [ciSup_le_iff (bddAbove_range _), ge_iff_le, Subtype.forall, isBase_restrict_iff',
+  simp only [ciSup_le_iff (bddAbove_range _), Subtype.forall, isBase_restrict_iff',
     comap_isBasis'_iff, and_imp]
   refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩
   · rw [← mk_image_eq_of_injOn_lift _ _ hfI, lift_le]
diff --git a/Mathlib/Data/Sum/Order.lean b/Mathlib/Data/Sum/Order.lean
index 0dfd26e5e7a551..ec34d24d499592 100644
--- a/Mathlib/Data/Sum/Order.lean
+++ b/Mathlib/Data/Sum/Order.lean
@@ -683,8 +683,7 @@ def sumLexDualAntidistrib (α β : Type*) [LE α] [LE β] : (α ⊕ₗ β)ᵒᵈ
   { Equiv.sumComm α β with
     map_rel_iff' := fun {a b} => by
       rcases a with (a | a) <;> rcases b with (b | b)
-      · simp only [ge_iff_le]
-        change
+      · change
           toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔
             toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)
         simp [toDual_le_toDual]
diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
index 871eeed26bfc62..b517148afe96ff 100644
--- a/Mathlib/GroupTheory/CoprodI.lean
+++ b/Mathlib/GroupTheory/CoprodI.lean
@@ -528,7 +528,7 @@ theorem mem_smul_iff {i j : ι} {m₁ : M i} {m₂ : M j} {w : Word M} :
             subst h
             rfl
           · simp only [fstIdx, Option.map_eq_some_iff, Sigma.exists,
-              exists_and_right, exists_eq_right, not_exists, ne_eq] at hm'
+              exists_and_right, exists_eq_right, not_exists] at hm'
             exact (hm'.1 (w.toList.head hnil).2 (by rw [List.head?_eq_some_head])).elim
       · revert h
         rw [fstIdx]
diff --git a/Mathlib/Order/Hom/BoundedLattice.lean b/Mathlib/Order/Hom/BoundedLattice.lean
index 3bffcd3dfd2619..e1da2cbbf02f1d 100644
--- a/Mathlib/Order/Hom/BoundedLattice.lean
+++ b/Mathlib/Order/Hom/BoundedLattice.lean
@@ -325,10 +325,6 @@ instance : OrderBot (SupBotHom α β) where
   bot := ⟨⊥, rfl⟩
   bot_le _ _ := bot_le
 
-@[simp]
-theorem coe_sup (f g : SupBotHom α β) : DFunLike.coe (f ⊔ g) = f ⊔ g :=
-  rfl
-
 @[simp]
 theorem coe_bot : ⇑(⊥ : SupBotHom α β) = ⊥ :=
   rfl
@@ -475,10 +471,6 @@ instance : OrderTop (InfTopHom α β) where
   top := ⟨⊤, rfl⟩
   le_top _ _ := le_top
 
-@[simp]
-theorem coe_inf (f g : InfTopHom α β) : DFunLike.coe (f ⊓ g) = f ⊓ g :=
-  rfl
-
 @[simp]
 theorem coe_top : ⇑(⊤ : InfTopHom α β) = ⊤ :=
   rfl
diff --git a/Mathlib/Order/Hom/Lattice.lean b/Mathlib/Order/Hom/Lattice.lean
index f905588f9f6589..1aa364bcec569b 100644
--- a/Mathlib/Order/Hom/Lattice.lean
+++ b/Mathlib/Order/Hom/Lattice.lean
@@ -307,10 +307,6 @@ instance [OrderTop β] : OrderTop (SupHom α β) :=
 instance [BoundedOrder β] : BoundedOrder (SupHom α β) :=
   BoundedOrder.lift ((↑) : _ → α → β) (fun _ _ => id) rfl rfl
 
-@[simp]
-theorem coe_sup (f g : SupHom α β) : DFunLike.coe (f ⊔ g) = f ⊔ g :=
-  rfl
-
 @[simp]
 theorem coe_bot [Bot β] : ⇑(⊥ : SupHom α β) = ⊥ :=
   rfl
@@ -489,10 +485,6 @@ instance [OrderTop β] : OrderTop (InfHom α β) :=
 instance [BoundedOrder β] : BoundedOrder (InfHom α β) :=
   BoundedOrder.lift ((↑) : _ → α → β) (fun _ _ => id) rfl rfl
 
-@[simp]
-theorem coe_inf (f g : InfHom α β) : DFunLike.coe (f ⊓ g) = f ⊓ g :=
-  rfl
-
 @[simp]
 theorem coe_bot [Bot β] : ⇑(⊥ : InfHom α β) = ⊥ :=
   rfl
diff --git a/Mathlib/RingTheory/Ideal/Prod.lean b/Mathlib/RingTheory/Ideal/Prod.lean
index f9487d4eb2ff71..86a5e27fcceb58 100644
--- a/Mathlib/RingTheory/Ideal/Prod.lean
+++ b/Mathlib/RingTheory/Ideal/Prod.lean
@@ -99,7 +99,7 @@ def idealProdEquiv : Ideal (R × S) ≃o Ideal R × Ideal S where
   left_inv I := (ideal_prod_eq I).symm
   right_inv := fun ⟨I, J⟩ => by simp
   map_rel_iff' {I J} := by
-    simp only [Equiv.coe_fn_mk, ge_iff_le, Prod.mk_le_mk]
+    simp only [Equiv.coe_fn_mk, Prod.mk_le_mk]
     refine ⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩
     rw [ideal_prod_eq I, ideal_prod_eq J]
     exact inf_le_inf (comap_mono h.1) (comap_mono h.2)
diff --git a/lake-manifest.json b/lake-manifest.json
index 179d5781ab5547..afcfad13292d96 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "db33a0238d18dc67cadd81b3fdac53f82b950bb6",
+   "rev": "9c112c8bae8ce3141043e2a33c7c5f82d5ec2f91",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-12225",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index f5b1400d090473..3c2cb203b6c666 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-12225"
 require "leanprover-community" / "Qq" @ git "nightly-testing"
 require "leanprover-community" / "aesop" @ git "nightly-testing"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.86" -- ProofWidgets should always be pinned to a specific version
diff --git a/lean-toolchain b/lean-toolchain
index 33223b1e99f358..49380112fc86e7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-28
+leanprover/lean4-pr-releases:pr-release-12225-4e50b32