--- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Sun Jul 07 22:25:34 2024 +0100
+++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Mon Jul 08 22:27:50 2024 +0100
@@ -1157,7 +1157,7 @@
     have "ln (real (n + 1) / L) \<le> 0"
       using * eventually_at_top_dense by (intro tendsto_lowerbound [OF 0]) auto
     then have "n+1 \<le> L"
-      by (simp add: ln_div)
+      using \<open>0 < L\<close> by (simp add: ln_div)
     then show ?thesis
       using L_le by linarith
   qed