--- a/src/HOL/ex/HarmonicSeries.thy	Sun May 05 15:31:08 2024 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy	Mon May 06 14:39:33 2024 +0100
@@ -103,7 +103,7 @@
         by (simp add: tmdef)
       also from mgt0 have
         "\<dots> = ((1/(real tm)) * real ((2::nat)^(m - 1)))"
-        by (auto simp: tmdef dest: two_pow_sub)
+        using tmdef two_pow_sub by presburger
       also have
         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"
         by (simp add: tmdef)