diff -r df1150ec6cd7 -r 2c86ea8961b5 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Thu Mar 02 11:34:54 2023 +0000
+++ b/src/HOL/Analysis/Convex.thy	Thu Mar 02 17:17:18 2023 +0000
@@ -2369,9 +2369,6 @@
     using hull_inc u by fastforce
 qed
 
-lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
-  by (simp add: inner_sum_left sum.If_cases inner_Basis)
-
 lemma convex_set_plus:
   assumes "convex S" and "convex T" shows "convex (S + T)"
 proof -