src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 70346 408e15cbd2a6
parent 70136 f03a01a18c6e
child 70380 2b0dca68c3ee
     1.1 --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -131,8 +131,10 @@
     1.4        show "\<lbrakk>\<not> 0 \<le> m; a \<le> b;  x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk>
     1.5              \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
     1.6          apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
     1.7 -        apply (auto simp: diff_le_eq neg_le_divideR_eq)
     1.8 -        using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce
     1.9 +        apply (auto simp add: neg_le_divideR_eq not_le)
    1.10 +         apply (auto simp: field_simps)
    1.11 +        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)
    1.12 +        done
    1.13      qed
    1.14    qed
    1.15  qed