src/HOL/Analysis/Change_Of_Vars.thy

                 then have "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) = norm (f' x (y - x) /\<^sub>R r - (f y - f x) /\<^sub>R r)"
                   by (simp add: dist_norm)
                 also have "\<dots> = norm (f' x (y - x) - (f y - f x)) / r"
                   using \<open>r > 0\<close> by (simp add: divide_simps scale_right_diff_distrib [symmetric])
                 also have "\<dots> \<le> norm (f y - (f x + f' x (y - x))) / norm (y - x)"
-                  using that \<open>r > 0\<close> False by (simp add: algebra_simps field_split_simps dist_norm norm_minus_commute mult_right_mono)
+                  using that \<open>r > 0\<close> False by (simp add: field_split_simps dist_norm norm_minus_commute mult_right_mono)
                 also have "\<dots> < k"
                   using that \<open>0 < \<zeta>\<close> by (simp add: dist_commute r_def  \<zeta> [OF \<open>y \<in> S\<close> False])
                 finally show "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) < k" .
                 show "(y - x) /\<^sub>R r \<in> ball 0 1"
                   using that \<open>r > 0\<close> by (simp add: dist_norm divide_simps norm_minus_commute)

           have "(matrix (f' x) - B) *v w = 0" for w
           proof (rule lemma_partial_derivatives [of "(*v) (matrix (f' x) - B)"])
             show "linear ((*v) (matrix (f' x) - B))"
               by (rule matrix_vector_mul_linear)
             have "((\<lambda>y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
-              using tendsto_minus [OF lim_df] by (simp add: algebra_simps field_split_simps)
+              using tendsto_minus [OF lim_df] by (simp add: field_split_simps)
             then show "((\<lambda>y. (matrix (f' x) - B) *v (y - x) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
             proof (rule Lim_transform)
               have "((\<lambda>y. ((f y + B *v x - (f x + B *v y)) /\<^sub>R norm (y - x))) \<longlongrightarrow> 0) (at x within S)"
               proof (clarsimp simp add: Lim_within dist_norm)
                 fix e :: "real"

                 qed
               qed
               then show "((\<lambda>y. (matrix (f' x) - B) *v (y - x) /\<^sub>R
                            norm (y - x) - (f x + f' x (y - x) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0)
                           (at x within S)"
-                by (simp add: algebra_simps diff lin_df matrix_vector_mul_linear scalar_mult_eq_scaleR)
+                by (simp add: algebra_simps diff lin_df scalar_mult_eq_scaleR)
             qed
           qed (use x in \<open>simp; auto simp: not_less\<close>)
           ultimately have "f' x = (*v) B"
             by (force simp: algebra_simps scalar_mult_eq_scaleR)
           show "matrix (f' x) $ m $ n \<le> b"

         with subT show "f ` (K \<inter> S) \<subseteq> T" by blast
         show "?\<mu> T \<le> e / (2*c) ^ ?m * ?\<mu> K"
         proof (rule order_trans [OF measT])
           have "?DVU = (d * 2 * (4 * B) ^ (?n - 1)) * norm (v - u)^?n"
             using \<open>c > 0\<close>
-            apply (simp add: algebra_simps power_mult_distrib)
+            apply (simp add: algebra_simps)
             by (metis Suc_pred power_Suc zero_less_card_finite)
           also have "\<dots> \<le> (e / (2*c) ^ ?m / (?m ^ ?m)) * norm(v - u) ^ ?n"
             by (rule mult_right_mono [OF d]) auto
           also have "\<dots> \<le> e / (2*c) ^ ?m * ?\<mu> K"
           proof -

           by simp
         also have "\<dots> \<le> (2 ^ ?m * c ^ ?m)"
           using \<open>c > 0\<close> by (simp add: content_cbox_if_cart)
         finally have "sum ?\<mu> \<F> \<le> (2 ^ ?m * c ^ ?m)" .
         then show ?thesis
-          using \<open>e > 0\<close> \<open>c > 0\<close> by (auto simp: field_split_simps mult_less_0_iff)
+          using \<open>e > 0\<close> \<open>c > 0\<close> by (auto simp: field_split_simps)
       qed
       finally show ?thesis .
     qed
     show "\<exists>T. f ` S \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
     proof (intro exI conjI)

         apply (rule measure_differentiable_image [OF h_lmeas _ int_det])
         apply (blast intro: has_derivative_within_subset [OF der_g])
         done
       ultimately show ?thesis
         using \<open>y > 0\<close> integral_restrict_Int [of S "{t. h n (g t) = y}" "\<lambda>t. \<bar>det (matrix (g' t))\<bar> * y"]
-        apply (simp add: integrable_on_indicator integrable_on_cmult_iff integral_indicator)
+        apply (simp add: integrable_on_indicator integral_indicator)
         apply (simp add: indicator_def if_distrib cong: if_cong)
         done
     qed
     have hn_int: "h n integrable_on g ` S"
       apply (subst hn_eq)