src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

       done
   }
   then have "ball (x - e *\<^sub>R (x - c)) (e*d) \<inter> affine hull S \<subseteq> S"
     by auto
   moreover have "e * d > 0"
-    using `e > 0` `d > 0` by (rule mult_pos_pos)
+    using `e > 0` `d > 0` by simp
   moreover have c: "c \<in> S"
     using assms rel_interior_subset by auto
   moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
     using mem_convex[of S x c e]
     apply (simp add: algebra_simps)

   have "\<exists>y \<in> S. norm (y - x) * (1 - e) < e * d"
   proof (cases "x \<in> S")
     case True
     then show ?thesis using `e > 0` `d > 0`
       apply (rule_tac bexI[where x=x])
-      apply (auto intro!: mult_pos_pos)
+      apply (auto)
       done
   next
     case False
     then have x: "x islimpt S"
       using assms(3)[unfolded closure_def] by auto

         apply auto
         done
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
-        using `e \<le> 1` `e > 0` `d > 0`
-        by (auto intro!:mult_pos_pos divide_pos_pos)
+        using `e \<le> 1` `e > 0` `d > 0` by (auto)
       then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
       then show ?thesis
         apply (rule_tac x=y in bexI)
         unfolding dist_norm

      using assms Real_Vector_Spaces.bounded_linear.pos_bounded[of f] by auto
     def e1 \<equiv> "1 / K"
     then have e1: "e1 > 0" "\<And>x. e1 * norm (f x) \<le> norm x"
       using K pos_le_divide_eq[of e1] by auto
     def e \<equiv> "e1 * e2"
-    then have "e > 0" using e1 e2 mult_pos_pos by auto
+    then have "e > 0" using e1 e2 by auto
     {
       fix y
       assume y: "y \<in> cball x e \<inter> affine hull S"
       then have h1: "f y \<in> affine hull (f ` S)"
         using affine_hull_linear_image[of f S] assms by auto

     then obtain e1 where e1: "e1 > 0" "\<forall>x \<in> span S. e1 * norm x \<le> norm (f x)"
       using assms injective_imp_isometric[of "span S" f]
         subspace_span[of S] closed_subspace[of "span S"]
       by auto
     def e \<equiv> "e1 * e2"
-    then have "e > 0"
-      using e1 e2 mult_pos_pos by auto
+    hence "e > 0" using e1 e2 by auto
     {
       fix y
       assume y: "y \<in> cball (f x) e \<inter> affine hull (f ` S)"
       then have "y \<in> f ` (affine hull S)"
         using affine_hull_linear_image[of f S] assms by auto

           using `t > 0` * `e > 0` by (auto simp add: field_simps)
         finally have "f x - f y < e" by auto
       }
       ultimately show ?thesis by auto
     qed (insert `0<e`, auto)
-  qed (insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos)
+  qed (insert `0<e` `0<k` `0<B`, auto simp: field_simps)
 qed
 
 
 subsection {* Upper bound on a ball implies upper and lower bounds *}
 

       apply (rule d[unfolded subset_eq,rule_format])
       unfolding mem_ball
       using assms(3-5)
       apply auto
       done
-  qed (rule mult_pos_pos, insert `e>0` `d>0`, auto)
+  qed (insert `e>0` `d>0`, auto)
 qed
 
 lemma mem_interior_closure_convex_shrink:
   fixes s :: "'a::euclidean_space set"
   assumes "convex s"

   proof (cases "x \<in> s")
     case True
     then show ?thesis
       using `e > 0` `d > 0`
       apply (rule_tac bexI[where x=x])
-      apply (auto intro!: mult_pos_pos)
+      apply (auto)
       done
   next
     case False
     then have x: "x islimpt s"
       using assms(3)[unfolded closure_def] by auto

         apply auto
         done
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
-        using `e \<le> 1` `e > 0` `d > 0`
-        by (auto intro!:mult_pos_pos divide_pos_pos)
+        using `e \<le> 1` `e > 0` `d > 0` by auto
       then obtain y where "y \<in> s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
       then show ?thesis
         apply (rule_tac x=y in bexI)
         unfolding dist_norm