diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Sun May 05 15:31:08 2024 +0100
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Mon May 06 14:39:33 2024 +0100
@@ -4219,14 +4219,17 @@
   hence "eventually (\<lambda>x. ?h x = g x - c * ln (b x) - 
            eval (C - const_expansion c * L) x * b x powr e) at_top" 
     (is "eventually (\<lambda>x. _ = ?h x) _") using assms(2)
-    by (auto simp: expands_to.simps scale_ms_def elim: eventually_elim2)
-  ultimately have **: "is_expansion_aux xs ?h (b # basis)" by (rule is_expansion_aux_cong)
+    apply (simp add: expands_to.simps scale_ms_def)
+    by (smt (verit) eventually_cong)
+  ultimately have **: "is_expansion_aux xs ?h (b # basis)" 
+    by (rule is_expansion_aux_cong)
   from assms(1,4) have "ms_exp_gt 0 (ms_aux_hd_exp xs)" "is_expansion C basis"
     by (auto simp: expands_to.simps elim!: is_expansion_aux_MSLCons)
   moreover from assms(1) have "length basis = expansion_level TYPE('a)"
     by (auto simp: expands_to.simps dest: is_expansion_aux_expansion_level)
   ultimately have "is_expansion_aux (MSLCons (C - scale_ms c L, e) xs) 
-                     (\<lambda>x. g x - c * ln (b x)) (b # basis)" using assms unfolding scale_ms_def
+                     (\<lambda>x. g x - c * ln (b x)) (b # basis)" 
+    using assms unfolding scale_ms_def
     by (intro is_expansion_aux.intros is_expansion_minus is_expansion_mult is_expansion_const * **)
        (simp_all add: basis_wf_Cons expands_to.simps)
   with assms(1) show ?thesis by (auto simp: expands_to.simps)