src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

     then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
       using span_insert_0[of "op + (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
     moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
       by auto
     moreover have "insert a (s - {a}) = insert a s"
-      using assms by auto
+      by auto
     ultimately have ?thesis
-      using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
+      using affine_hull_insert_span[of "a" "s-{a}"] by auto
   }
   ultimately show ?thesis by auto
 qed
 
 lemma affine_hull_span2:

   shows "aff_dim S \<le> int (DIM('n))"
 proof -
   have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
     using aff_dim_UNIV by auto
   then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
-    using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
+    using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
 qed
 
 lemma affine_dim_equal:
   fixes S :: "'n::euclidean_space set"
   assumes "affine S" "affine T" "S \<noteq> {}" "S \<subseteq> T" "aff_dim S = aff_dim T"