--- a/src/HOL/Analysis/Linear_Algebra.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue May 17 14:10:14 2022 +0100
@@ -1167,7 +1167,7 @@
next
assume ?rhs
then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
- by (auto simp: )
+ by auto
have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y
by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
then show ?lhs