src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
   by (simp add: subspace_def)
 
 lemma delta_mult_idempotent:
   "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
-  by (cases "k=a") auto
+  by simp
 
 lemma setsum_UNIV_sum:
   fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
   shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
   apply (subst UNIV_Plus_UNIV [symmetric])

       from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m"
         where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
       have "x \<in> span (columns A)"
         unfolding y[symmetric]
         apply (rule span_setsum)
-        apply clarify
         unfolding scalar_mult_eq_scaleR
         apply (rule span_mul)
         apply (rule span_superset)
         unfolding columns_def
         apply blast