diff -r 1b0fc6ceb750 -r bb5d036f3523 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Thu Jan 25 17:08:07 2024 +0000
+++ b/src/HOL/Analysis/Convex.thy	Fri Jan 26 11:19:22 2024 +0000
@@ -911,14 +911,10 @@
 next
   case True
   define r where "r \<equiv> (\<Sum>i\<in>I. a i * b i) / (\<Sum>i\<in>I. (b i)\<^sup>2)"
-  with True have *: "(\<Sum>i\<in>I. a i * b i) = r * (\<Sum>i\<in>I. (b i)\<^sup>2)"
-    by simp
   have "0 \<le> (\<Sum>i\<in>I. (a i - r * b i)\<^sup>2)"
-    by (meson sum_nonneg zero_le_power2)
+    by (simp add: sum_nonneg)
   also have "... = (\<Sum>i\<in>I. (a i)\<^sup>2) - 2 * r * (\<Sum>i\<in>I. a i * b i) + r\<^sup>2 * (\<Sum>i\<in>I. (b i)\<^sup>2)"
     by (simp add: algebra_simps power2_eq_square sum_distrib_left flip: sum.distrib)
-  also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - (\<Sum>i\<in>I. a i * b i) * r"
-    by (simp add: * power2_eq_square)
   also have "\<dots> = (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)"
     by (simp add: r_def power2_eq_square)
   finally have "0 \<le> (\<Sum>i\<in>I. (a i)\<^sup>2) - ((\<Sum>i\<in>I. a i * b i))\<^sup>2 / (\<Sum>i\<in>I. (b i)\<^sup>2)" .
@@ -2436,4 +2432,4 @@
   "convex hull (\<Sum>i\<in>A. B i) = (\<Sum>i\<in>A. convex hull (B i))"
   by (induction A rule: infinite_finite_induct) (auto simp: convex_hull_set_plus)
 
-end
\ No newline at end of file
+end