src/HOL/Real_Vector_Spaces.thy

--- a/src/HOL/Real_Vector_Spaces.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -553,7 +553,9 @@
 
 lemma scaleR_image_atLeastAtMost: "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
   apply (auto intro!: scaleR_left_mono simp: image_iff Bex_def)
-  by (meson local.eq_iff pos_divideR_le_eq pos_le_divideR_eq)
+  using pos_divideR_le_eq [of c] pos_le_divideR_eq [of c]
+  apply (meson local.order_eq_iff) 
+  done
 
 end