src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

     fix c :: real
     assume c: "c \<ge> 0"
     then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
       using x by (simp add: algebra_simps)
     moreover
-    have "c * cx \<ge> 0"
-      using c x using mult_nonneg_nonneg by auto
+    have "c * cx \<ge> 0" using c x by auto
     ultimately
     have "c *\<^sub>R x \<in> ?rhs" using x by auto
   }
   then have "cone ?rhs"
     unfolding cone_def by auto

         using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
       also have "\<dots> = u * v1 + v * v2"
         by simp
       finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
       have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
-        apply (rule add_nonneg_nonneg)
-        prefer 4
-        apply (rule add_nonneg_nonneg)
-        apply (rule_tac [!] mult_nonneg_nonneg)
-        using as(1,2) obt1(1,2) obt2(1,2)
-        apply auto
-        done
+        using as(1,2) obt1(1,2) obt2(1,2) by auto
       then show ?thesis
         unfolding obt1(5) obt2(5)
         unfolding * and **
         using False
         apply (rule_tac

       apply (rule conjI)
       defer
       apply (rule_tac x="1 - u * u1 - v * u2" in exI)
       unfolding Bex_def
       using as(1,2) obt1(1,2) obt2(1,2) **
-      apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
+      apply (auto simp add: algebra_simps)
       done
   qed
 qed
 
 

     show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and>
       (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
     proof (cases "i\<in>{1..k1}")
       case True
       then show ?thesis
-        using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]]
-        by auto
+        using uv(1) x(1)[THEN bspec[where x=i]] by auto
     next
       case False
       def j \<equiv> "i - k1"
       from i False have "j \<in> {1..k2}"
         unfolding j_def by auto
       then show ?thesis
-        unfolding j_def[symmetric]
-        using False
-        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]]
-        apply auto
-        done
+        using False uv(2) y(1)[THEN bspec[where x=j]]
+        by (auto simp: j_def[symmetric])
     qed
   qed (auto simp add: not_le x(2,3) y(2,3) uv(3))
 qed
 
 lemma convex_hull_finite:

   {
     fix x
     assume "x\<in>s"
     then have "0 \<le> u * ux x + v * uy x"
       using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
-      apply auto
-      apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))
-      done
+      by auto
   }
   moreover
   have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
     unfolding setsum_addf and setsum_right_distrib[symmetric] and ux(2) uy(2)
     using uv(3) by auto

       then have v: "0 \<le> u v"
         using obt(4)[THEN bspec[where x=v]] by auto
       show "0 \<le> u v + t * w v"
       proof (cases "w v < 0")
         case False
-        then show ?thesis
-          apply (rule_tac add_nonneg_nonneg)
-          using v
-          apply simp
-          apply (rule mult_nonneg_nonneg)
-          using `t\<ge>0`
-          apply auto
-          done
+        thus ?thesis using v `t\<ge>0` by auto
       next
         case True
         then have "t \<le> u v / (- w v)"
           using `v\<in>s`
           unfolding t_def i_def

       by auto
     then have "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)"
       apply (rule_tac x = "inverse(norm a) *\<^sub>R a" in exI)
       using hull_subset[of c convex]
       unfolding subset_eq and inner_scaleR
-      apply -
-      apply rule
-      defer
-      apply rule
-      apply (rule mult_nonneg_nonneg)
-      apply (auto simp add: inner_commute del: ballE elim!: ballE)
-      done
+      by (auto simp add: inner_commute del: ballE elim!: ballE)
     then show "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}"
       unfolding c(1) frontier_cball dist_norm by auto
   qed (insert closed_halfspace_ge, auto)
   then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y"
     unfolding frontier_cball dist_norm by auto

     assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
     have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
       using assms as(1)[unfolded mem_box]
       apply (erule_tac x=i in ballE)
       apply rule
-      apply (rule mult_nonneg_nonneg)
-      prefer 3
+      prefer 2
       apply (rule mult_right_le_one_le)
       using assms
       apply auto
       done
     then show "y \<in> cbox (x - ?d) (x + ?d)"

     from xy obtain d t where
       yc: "y = setsum (\<lambda>i. d i *\<^sub>R t i) I \<and> (\<forall>i\<in>I. d i \<ge> 0) \<and> setsum d I = 1 \<and> (\<forall>i\<in>I. t i \<in> S i)"
       by auto
     def e \<equiv> "\<lambda>i. u * c i + v * d i"
     have ge0: "\<forall>i\<in>I. e i \<ge> 0"
-      using e_def xc yc uv by (simp add: mult_nonneg_nonneg)
+      using e_def xc yc uv by simp
     have "setsum (\<lambda>i. u * c i) I = u * setsum c I"
       by (simp add: setsum_right_distrib)
     moreover have "setsum (\<lambda>i. v * d i) I = v * setsum d I"
       by (simp add: setsum_right_distrib)
     ultimately have sum1: "setsum e I = 1"

         case False
         then show ?thesis
           using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
             mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
             assms q_def e_def i False xc yc uv
-          by auto
+          by (auto simp del: mult_nonneg_nonneg)
       qed
     }
     then have qs: "\<forall>i\<in>I. q i \<in> S i" by auto
     {
       fix i
       assume i: "i \<in> I"
       have "(u * c i) *\<^sub>R s i + (v * d i) *\<^sub>R t i = e i *\<^sub>R q i"
       proof (cases "e i = 0")
         case True
         have ge: "u * (c i) \<ge> 0 \<and> v * d i \<ge> 0"
-          using xc yc uv i by (simp add: mult_nonneg_nonneg)
+          using xc yc uv i by simp
         moreover from ge have "u * c i \<le> 0 \<and> v * d i \<le> 0"
           using True e_def i by simp
         ultimately have "u * c i = 0 \<and> v * d i = 0" by auto
         with True show ?thesis by auto
       next