src/HOL/Analysis/Elementary_Normed_Spaces.thy

     show "?rhs \<subseteq> ?lhs"
     proof (clarsimp, intro conjI impI subsetI)
       show "\<lbrakk>0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}\<rbrakk>
             \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
         apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
-        using False apply (auto simp: le_diff_eq pos_le_divideRI)
-        using diff_le_eq pos_le_divideR_eq by force
+        using False apply (auto simp: pos_le_divideR_eq pos_divideR_le_eq le_diff_eq diff_le_eq)
+        done
       show "\<lbrakk>\<not> 0 \<le> m; a \<le> b;  x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk>
             \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
         apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
-        apply (auto simp add: neg_le_divideR_eq not_le)
-         apply (auto simp: field_simps)
-        apply (metis (no_types, lifting) add_diff_cancel_left' add_le_imp_le_right diff_add_cancel inverse_eq_divide neg_le_divideR_eq neg_le_iff_le scale_minus_right)
+         apply (auto simp add: neg_le_divideR_eq neg_divideR_le_eq not_le le_diff_eq diff_le_eq)
         done
     qed
   qed
 qed
 

       and "continuous_on S f"
       and "finite (f ` S)"
     shows "f constant_on S"
   using assms continuous_finite_range_constant_eq  by blast
 
-
 end