diff -r f3d19c8445ec -r 24b70433c2e8 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue May 30 12:07:48 2023 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue May 30 12:33:06 2023 +0100
@@ -901,7 +901,7 @@
   fixes x :: "'a::euclidean_space"
   shows "norm x \<le> sqrt DIM('a) * infnorm x"
   unfolding norm_eq_sqrt_inner id_def
-proof (rule real_le_lsqrt[OF inner_ge_zero])
+proof (rule real_le_lsqrt)
   show "sqrt DIM('a) * infnorm x \<ge> 0"
     by (simp add: zero_le_mult_iff infnorm_pos_le)
   have "x \<bullet> x \<le> (\<Sum>b\<in>Basis. x \<bullet> b * (x \<bullet> b))"