diff --git a/Mathlib/Algebra/AddTorsor.lean b/Mathlib/Algebra/AddTorsor.lean
index f9baa6191726f..32963195471d0 100644
--- a/Mathlib/Algebra/AddTorsor.lean
+++ b/Mathlib/Algebra/AddTorsor.lean
@@ -248,7 +248,6 @@ instance instAddTorsor : AddTorsor (G × G') (P × P') where
   zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
   add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)
   vsub p₁ p₂ := (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2)
-  nonempty := Prod.instNonempty
   vsub_vadd' _ _ := Prod.ext (vsub_vadd _ _) (vsub_vadd _ _)
   vadd_vsub' _ _ := Prod.ext (vadd_vsub _ _) (vadd_vsub _ _)
 
diff --git a/Mathlib/Logic/Nonempty.lean b/Mathlib/Logic/Nonempty.lean
index 1a52ca02ab2d4..1c8198b9475d3 100644
--- a/Mathlib/Logic/Nonempty.lean
+++ b/Mathlib/Logic/Nonempty.lean
@@ -99,13 +99,6 @@ theorem Nonempty.elim_to_inhabited {α : Sort*} [h : Nonempty α] {p : Prop} (f
     p :=
   h.elim <| f ∘ Inhabited.mk
 
-protected instance Prod.instNonempty {α β} [h : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
-  h.elim fun g ↦ h2.elim fun g2 ↦ ⟨⟨g, g2⟩⟩
-
-protected instance Pi.instNonempty {ι : Sort*} {α : ι → Sort*} [∀ i, Nonempty (α i)] :
-    Nonempty (∀ i, α i) :=
-  ⟨fun _ ↦ Classical.arbitrary _⟩
-
 theorem Classical.nonempty_pi {ι} {α : ι → Sort*} : Nonempty (∀ i, α i) ↔ ∀ i, Nonempty (α i) :=
   ⟨fun ⟨f⟩ a ↦ ⟨f a⟩, @Pi.instNonempty _ _⟩
 
diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
index 4eae4a2c7b4eb..f828a823ee8cd 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
@@ -157,9 +157,9 @@ open UniformConvergence
 
 variable {α β : Type*} {𝔖 : Set (Set α)}
 
-instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty
+instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty _
 
-instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty
+instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty _
 
 instance [Subsingleton β] : Subsingleton (α →ᵤ β) :=
   inferInstanceAs <| Subsingleton <| α → β
diff --git a/lake-manifest.json b/lake-manifest.json
index ac14cbf86e7d7..ed832574476f2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6823ca35a23905867f0c6d9678932e6f261157e4",
+   "rev": "c37494a698d68c5e3711575fcb90ebf2974900ff",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index a5551df349f89..98d327efee081 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-09-23
+leanprover/lean4:nightly-2024-09-24