src/HOL/Analysis/Linear_Algebra.thy

     by (metis span_superset span_mono subset_trans)
   from span_mono[OF B(3)] C have SVC: "span V \<subseteq> span C"
     by (simp add: span_span)
   from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
   have iC: "independent C"
-    by (simp add: dim_span)
+    by (simp)
   from C fB have "card C \<le> dim V"
     by simp
   moreover have "dim V \<le> card C"
     using span_card_ge_dim[OF CSV SVC C(1)]
     by simp

   then obtain b where b: "b \<noteq> 0" "span S \<subseteq> {a. b \<bullet> a = 0}"
     using lowdim_subset_hyperplane [of S] by fastforce
   show ?thesis
     apply (rule that[OF b(1)])
     apply (rule subspace_dim_equal)
-    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
-        subspace_span)
+    by (auto simp: assms b dim_hyperplane subspace_hyperplane)
 qed
 
 lemma dim_eq_hyperplane:
   fixes S :: "'n::euclidean_space set"
   shows "dim S = DIM('n) - 1 \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> span S = {x. a \<bullet> x = 0})"
 by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)
 
 
-subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
+subsection\<open> Orthogonal bases and Gram-Schmidt process\<close>
 
 lemma pairwise_orthogonal_independent:
   assumes "pairwise orthogonal S" and "0 \<notin> S"
     shows "independent S"
 proof -

     by (simp add: S pairwise_orthogonal_imp_finite)
   have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
        if "x \<in> S" for x
   proof -
     have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
-      by (simp add: \<open>finite S\<close> inner_commute sum.delta that)
+      by (simp add: \<open>finite S\<close> inner_commute that)
     also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
       apply (rule sum.cong [OF refl], simp)
       by (meson S orthogonal_def pairwise_def that)
    finally show ?thesis
      by (simp add: orthogonal_def algebra_simps inner_sum_left)

   obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
 proof -
   obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
              and "independent B" "card B = dim S" "span B = span S"
-    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
-      (auto simp: dim_span)
+    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span]) (auto)
   with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
     by auto
   obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
     by (blast intro: orthogonal_extension [OF orthB])
   show thesis

 corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_subspace_exists:
   fixes S :: "'a :: euclidean_space set"
   assumes "dim S < DIM('a)"
   obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
 proof -
-have "span S \<subset> UNIV"
+  have "span S \<subset> UNIV"
   by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
       mem_Collect_eq top.extremum_strict top.not_eq_extremum)
   with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
-    by (auto simp: span_UNIV)
+    by (auto)
 qed
 
 corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_vector_exists:
   fixes x :: "'a :: euclidean_space"
   assumes "2 \<le> DIM('a)"

       by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
     show "finite (S - {0})"
       using \<open>independent (S - {0})\<close> independent_imp_finite by blast
     show "card (S - {0}) = DIM('a)"
       using span_delete_0 [of S] S
-      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
+      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
   qed (use S \<open>a \<noteq> 0\<close> in auto)
 qed
 
 lemma vector_in_orthonormal_basis:
   fixes a :: "'a::euclidean_space"

   have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     using 1 by (simp add: span_induct [OF _ subspace_hyperplane])
   then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
     by simp
   have "dim(A \<union> B) = dim (span (A \<union> B))"
-    by (simp add: dim_span)
+    by (simp)
   also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
     by (auto simp add: span_Un image_def)
   also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
     by (auto intro!: arg_cong [where f=dim])
   also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
     by (auto simp: dest: 0)
   also have "... = dim (span A) + dim (span B)"
-    by (rule dim_sums_Int) (auto simp: subspace_span)
+    by (rule dim_sums_Int) (auto)
   also have "... = dim A + dim B"
-    by (simp add: dim_span)
+    by (simp)
   finally show ?thesis .
 qed
 
 lemma dim_subspace_orthogonal_to_vectors:
   fixes A :: "'a::euclidean_space set"

       then show ?thesis
         apply (auto simp: span_Un image_def  \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
         using \<open>y \<in> span A\<close> add.commute by blast
     qed
     show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
-      by (rule span_minimal)
-        (auto intro: * span_minimal simp: subspace_span)
+      by (rule span_minimal) (auto intro: * span_minimal)
   qed
   then show ?thesis
     by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
         orthogonal_commute orthogonal_def)
 qed

         unfolding dist_norm
       proof (rule eventually_mono)
         show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x
           using that B
           apply (simp add: field_split_simps)
-          by (metis \<open>linear h\<close> le_less_trans linear_diff mult.commute)
+          by (metis \<open>linear h\<close> le_less_trans linear_diff)
       qed
     qed
   qed
 qed