diff --git a/Mathlib/RingTheory/Valuation/Discrete/Basic.lean b/Mathlib/RingTheory/Valuation/Discrete/Basic.lean
index fbf93ea3a334e7..714a41abbc2391 100644
--- a/Mathlib/RingTheory/Valuation/Discrete/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/Discrete/Basic.lean
@@ -132,7 +132,16 @@ instance : v.IsNontrivial := by
     intro y x
     specialize h1 x
     aesop
+  #adaptation_note
+  /-- Until nightly-2026-01-07, this was:
+  ```
   aesop (add safe forward [generator_lt_one, generator_zpowers_eq_valueGroup])
+  ```
+  -/
+  simp_all only [ne_eq]
+  have : generator v < 1 := generator_lt_one v
+  have : zpowers (generator v) = valueGroup v := generator_zpowers_eq_valueGroup v
+  simp_all only [zpowers_eq_bot, lt_self_iff_false]
 
 lemma valueGroup_genLTOne_eq_generator : (valueGroup v).genLTOne = generator v :=
   ((valueGroup v).genLTOne_unique (generator_lt_one v) (generator_zpowers_eq_valueGroup v)).symm
diff --git a/lake-manifest.json b/lake-manifest.json
index 5a9e1fb7226549..9f76f3996166f9 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b397d9226a96d388e740db11c33e14430369c0bf",
+   "rev": "78da9217f81ae1daa7b396f8e43da3f77fb30f68",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index f1ede4da8507dc..0421317bfaaf01 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-07
+leanprover/lean4:nightly-2026-01-09