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/lean-toolchain b/lean-toolchain
index f1ede4da8507dc..2654dd84f731ea 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-07
+leanprover/lean4:nightly-2026-01-08