# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1691169469 -7200
# Node ID 37abfe400ae69e6286009751da0ffffa1fc430e3
# Parent  032a4344903e867e2b0dd0cf8979d41e4b2e7aac
Removal of ugly old proofs

diff -r 032a4344903e -r 37abfe400ae6 src/HOL/Analysis/Line_Segment.thy
--- a/src/HOL/Analysis/Line_Segment.thy	Thu Aug 03 19:10:43 2023 +0200
+++ b/src/HOL/Analysis/Line_Segment.thy	Fri Aug 04 19:17:49 2023 +0200
@@ -33,24 +33,13 @@
 lemma sphere_eq_empty [simp]:
   fixes a :: "'a::{real_normed_vector, perfect_space}"
   shows "sphere a r = {} \<longleftrightarrow> r < 0"
-by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist)
+  by (metis empty_iff linorder_not_less mem_sphere sphere_empty vector_choose_dist)
 
 lemma cone_closure:
   fixes S :: "'a::real_normed_vector set"
   assumes "cone S"
   shows "cone (closure S)"
-proof (cases "S = {}")
-  case True
-  then show ?thesis by auto
-next
-  case False
-  then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
-    using cone_iff[of S] assms by auto
-  then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
-    using closure_subset by (auto simp: closure_scaleR)
-  then show ?thesis
-    using False cone_iff[of "closure S"] by auto
-qed
+  by (metis UnCI assms closure_Un_frontier closure_eq_empty closure_scaleR cone_iff)
 
 
 corollary component_complement_connected:
@@ -63,7 +52,7 @@
 proposition clopen:
   fixes S :: "'a :: real_normed_vector set"
   shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
-  by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
+  using  connected_UNIV by (force simp add: connected_clopen)
 
 corollary compact_open:
   fixes S :: "'a :: euclidean_space set"
@@ -97,20 +86,12 @@
   then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
     using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
   then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
-    using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
-    using assms(2)[unfolded convex_on_def,
-      THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
-    by auto
+    using \<open>x\<in>s\<close> \<open>y\<in>s\<close> by (smt (verit) assms(2) convex_on_def)
   moreover
   have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
     by (simp add: algebra_simps)
   have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
-    unfolding mem_ball dist_norm
-    unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>]
-    unfolding dist_norm[symmetric]
-    using u
-    unfolding pos_less_divide_eq[OF xy]
-    by auto
+    by (smt (verit) "*" \<open>0 < u\<close> dist_norm mem_ball norm_scaleR pos_less_divide_eq u xy)
   then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)"
     using assms(4) by auto
   ultimately show False
@@ -256,8 +237,8 @@
   using midpoint_eq_iff by metis
 
 lemma midpoint_linear_image:
-   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
-by (simp add: linear_iff midpoint_def)
+  "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+  by (simp add: linear_iff midpoint_def)
 
 
 subsection \<open>Open and closed segments\<close>
@@ -288,29 +269,24 @@
   by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
 
 lemma closed_segment_translation:
-    "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
-apply safe
-apply (rule_tac x="x-c" in image_eqI)
-apply (auto simp: in_segment algebra_simps)
-done
+    "closed_segment (c + a) (c + b) = (\<lambda>x. c + x) ` (closed_segment a b)" (is "?L = _ ` ?R")
+proof -
+  have "\<And>x. x \<in> ?L \<Longrightarrow> x - c \<in> ?R" "\<And>x. \<lbrakk>x \<in> ?R\<rbrakk> \<Longrightarrow> c + x \<in> ?L"
+    by (auto simp: in_segment algebra_simps)
+  then show ?thesis by force
+qed
 
 lemma open_segment_translation:
-    "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
-by (simp add: open_segment_def closed_segment_translation translation_diff)
+  "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
+  by (simp add: open_segment_def closed_segment_translation translation_diff)
 
 lemma closed_segment_of_real:
     "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
-  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
-    apply (rule_tac x="(1-u)*x + u*y" in bexI)
-  apply (auto simp: in_segment)
-  done
+  by (simp add: closed_segment_linear_image linearI scaleR_conv_of_real)
 
 lemma open_segment_of_real:
     "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
-  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
-    apply (rule_tac x="(1-u)*x + u*y" in bexI)
-  apply (auto simp: in_segment)
-  done
+  by (simp add: closed_segment_of_real image_set_diff inj_of_real open_segment_def)
 
 lemma closed_segment_Reals:
     "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
@@ -333,13 +309,9 @@
     "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b"
 proof -
   have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)"
-    apply (simp add: closed_segment_def)
-    apply (erule ex_forward)
-    apply (simp add: algebra_simps)
-    done
+    using closed_segment_translation by blast
   show ?thesis
-  using * [where d = "-d"] *
-  by (fastforce simp add:)
+    using * [where d = "-d"] * by fastforce
 qed
 
 lemma open_segment_translation_eq [simp]:
@@ -348,13 +320,11 @@
 
 lemma of_real_closed_segment [simp]:
   "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b"
-  apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward)
-  using of_real_eq_iff by fastforce
+  by (simp add: closed_segment_of_real image_iff)
 
 lemma of_real_open_segment [simp]:
   "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b"
-  apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
-  using of_real_eq_iff by fastforce
+  by (simp add: image_iff open_segment_of_real)
 
 lemma convex_contains_segment:
   "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
@@ -389,12 +359,11 @@
 
 lemma segment_open_subset_closed:
    "open_segment a b \<subseteq> closed_segment a b"
-  by (auto simp: closed_segment_def open_segment_def)
+  by (simp add: open_closed_segment subsetI)
 
 lemma bounded_closed_segment:
   fixes a :: "'a::real_normed_vector" shows "bounded (closed_segment a b)"
-  by (rule boundedI[where B="max (norm a) (norm b)"])
-    (auto simp: closed_segment_def max_def convex_bound_le intro!: norm_triangle_le)
+  by (simp add: bounded_convex_hull segment_convex_hull)
 
 lemma bounded_open_segment:
     fixes a :: "'a::real_normed_vector" shows "bounded (open_segment a b)"
@@ -403,8 +372,7 @@
 lemmas bounded_segment = bounded_closed_segment open_closed_segment
 
 lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
-  unfolding segment_convex_hull
-  by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
+  by (simp_all add: hull_inc segment_convex_hull)
 
 
 lemma eventually_closed_segment:
@@ -420,10 +388,10 @@
   proof eventually_elim
     case (elim x)
     have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
-    from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
-    have "closed_segment x0 x \<subseteq> ball x0 e" .
-    also note \<open>\<dots> \<subseteq> X0\<close>
-    finally show ?case .
+    then have "closed_segment x0 x \<subseteq> ball x0 e"
+      using closed_segment_subset elim by blast 
+    then show ?case
+      using e(2) by auto 
   qed
 qed
 
@@ -438,26 +406,33 @@
   assumes "x \<in> closed_segment a b"
   shows "norm (x - a) \<le> norm (b - a)"
 proof -
-  obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
+  obtain u where u: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
     using assms by (auto simp add: closed_segment_def)
-  then show "norm (x - a) \<le> norm (b - a)"
-    apply clarify
-    apply (auto simp: algebra_simps)
-    apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
-    done
+  then have "norm (u *\<^sub>R b - u *\<^sub>R a) \<le> norm (b - a)"
+    by (simp add: mult_left_le_one_le flip: scaleR_diff_right)
+  with u show ?thesis
+    by (metis add_diff_cancel_left scaleR_collapse)
 qed
 
 lemma segment_bound:
   assumes "x \<in> closed_segment a b"
   shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
-by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+
+  by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+
+
+lemma open_segment_bound1:
+  assumes "x \<in> open_segment a b"
+  shows "norm (x - a) < norm (b - a)"
+proof -
+  obtain u where u: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1"
+    by (meson assms in_segment)
+  then have "norm (u *\<^sub>R b - u *\<^sub>R a) < norm (b - a)"
+    using assms in_segment(2) less_eq_real_def by (fastforce simp flip: scaleR_diff_right)
+  with u show ?thesis
+    by (metis add_diff_cancel_left scaleR_collapse)
+qed
 
 lemma open_segment_commute: "open_segment a b = open_segment b a"
-proof -
-  have "{a, b} = {b, a}" by auto
-  thus ?thesis
-    by (simp add: closed_segment_commute open_segment_def)
-qed
+  by (simp add: closed_segment_commute insert_commute open_segment_def)
 
 lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
   unfolding segment by (auto simp add: algebra_simps)
@@ -494,8 +469,7 @@
 lemma closed_segment_eq_real_ivl:
   fixes a b::real
   shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
-  using closed_segment_eq_real_ivl1[of a b] closed_segment_eq_real_ivl1[of b a]
-  by (auto simp: closed_segment_commute)
+  by (metis closed_segment_commute closed_segment_eq_real_ivl1 nle_le)
 
 lemma open_segment_eq_real_ivl:
   fixes a b::real
@@ -504,7 +478,7 @@
 
 lemma closed_segment_real_eq:
   fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
-  by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
+  by (simp add: closed_segment_eq_real_ivl image_affinity_atLeastAtMost)
 
 lemma closed_segment_same_Re:
   assumes "Re a = Re b"
@@ -546,57 +520,13 @@
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> closed_segment a b"
     shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
-proof (intro conjI)
-  obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
-    using assms by (force simp: in_segment algebra_simps)
-  have "dist x a = u * dist a b"
-    apply (simp add: dist_norm algebra_simps x)
-    by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
-  also have "...  \<le> dist a b"
-    by (simp add: mult_left_le_one_le u)
-  finally show "dist x a \<le> dist a b" .
-  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
-    by (simp add: dist_norm algebra_simps x)
-  also have "... = (1-u) * dist a b"
-  proof -
-    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
-      using \<open>u \<le> 1\<close> by force
-    then show ?thesis
-      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
-  qed
-  also have "... \<le> dist a b"
-    by (simp add: mult_left_le_one_le u)
-  finally show "dist x b \<le> dist a b" .
-qed
+  by (metis assms dist_commute dist_norm segment_bound(2) segment_bound1)
 
 lemma dist_in_open_segment:
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> open_segment a b"
-    shows "dist x a < dist a b \<and> dist x b < dist a b"
-proof (intro conjI)
-  obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
-    using assms by (force simp: in_segment algebra_simps)
-  have "dist x a = u * dist a b"
-    apply (simp add: dist_norm algebra_simps x)
-    by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
-  also have *: "...  < dist a b"
-    using assms mult_less_cancel_right2 u(2) by fastforce
-  finally show "dist x a < dist a b" .
-  have ab_ne0: "dist a b \<noteq> 0"
-    using * by fastforce
-  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
-    by (simp add: dist_norm algebra_simps x)
-  also have "... = (1-u) * dist a b"
-  proof -
-    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
-      using \<open>u < 1\<close> by force
-    then show ?thesis
-      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
-  qed
-  also have "... < dist a b"
-    using ab_ne0 \<open>0 < u\<close> by simp
-  finally show "dist x b < dist a b" .
-qed
+  shows "dist x a < dist a b \<and> dist x b < dist a b"
+  by (metis assms dist_commute dist_norm open_segment_bound1 open_segment_commute)
 
 lemma dist_decreases_open_segment_0:
   fixes x :: "'a :: euclidean_space"
@@ -650,9 +580,7 @@
   fixes a :: "'a :: euclidean_space"
   assumes "x \<in> closed_segment a b"
     shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
-apply (cases "x \<in> open_segment a b")
- using dist_decreases_open_segment less_eq_real_def apply blast
-by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
+  by (smt (verit, ccfv_threshold) Un_iff assms closed_segment_eq_open dist_norm empty_iff insertE open_segment_furthest_le)
 
 corollary segment_furthest_le:
   fixes a b x y :: "'a::euclidean_space"
@@ -663,19 +591,18 @@
 lemma convex_intermediate_ball:
   fixes a :: "'a :: euclidean_space"
   shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
-apply (simp add: convex_contains_open_segment, clarify)
-by (metis (no_types, opaque_lifting) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
+  by (smt (verit) convex_contains_open_segment dist_decreases_open_segment mem_ball mem_cball subset_eq)
 
 lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
   apply (clarsimp simp: midpoint_def in_segment)
   apply (rule_tac x="(1 + u) / 2" in exI)
-  apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
+  apply (simp add: algebra_simps add_divide_distrib diff_divide_distrib)
   by (metis field_sum_of_halves scaleR_left.add)
 
 lemma notin_segment_midpoint:
   fixes a :: "'a :: euclidean_space"
   shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
-by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
+  by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
 
 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
 
@@ -687,27 +614,18 @@
 lemma segment_degen_1:
   fixes a :: "'a :: real_vector"
   shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
-proof -
-  { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
-    then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
-      by (simp add: algebra_simps)
-    then have "a=b \<or> u=1"
-      by simp
-  } then show ?thesis
-      by (auto simp: algebra_simps)
-qed
+  by (smt (verit, best) add_right_cancel scaleR_cancel_left scaleR_collapse)
 
 lemma segment_degen_0:
     fixes a :: "'a :: real_vector"
     shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
-  using segment_degen_1 [of "1-u" b a]
-  by (auto simp: algebra_simps)
+  using segment_degen_1 [of "1-u" b a] by (auto simp: algebra_simps)
 
 lemma add_scaleR_degen:
   fixes a b ::"'a::real_vector"
   assumes  "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)"  "u \<noteq> v"
   shows "a=b"
-  by (metis (no_types, opaque_lifting) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
+  by (smt (verit) add_diff_cancel_left' add_diff_eq assms scaleR_cancel_left scaleR_left.diff)
   
 lemma closed_segment_image_interval:
      "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
@@ -723,14 +641,7 @@
   by auto
 
 lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
-proof -
-  { assume a1: "open_segment a b = {}"
-    have "{} \<noteq> {0::real<..<1}"
-      by simp
-    then have "a = b"
-      using a1 open_segment_image_interval by fastforce
-  } then show ?thesis by auto
-qed
+  by (simp add: segment_image_interval(2))
 
 lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
   using open_segment_eq_empty by blast
@@ -751,11 +662,9 @@
 qed
 
 lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
-  apply auto
-  apply (rule ccontr)
-  apply (simp add: segment_image_interval)
-  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
-  done
+  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment [of a b]]
+  unfolding segment_image_interval
+  by (smt (verit, del_insts) finite.emptyI finite_insert finite_subset image_subset_iff insertCI segment_degen_0)
 
 lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
   by (auto simp: open_segment_def)
@@ -770,19 +679,6 @@
 
 lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
 
-lemma open_segment_bound1:
-  assumes "x \<in> open_segment a b"
-  shows "norm (x - a) < norm (b - a)"
-proof -
-  obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
-    using assms by (auto simp add: open_segment_image_interval split: if_split_asm)
-  then show "norm (x - a) < norm (b - a)"
-    apply clarify
-    apply (auto simp: algebra_simps)
-    apply (simp add: scaleR_diff_right [symmetric])
-    done
-qed
-
 lemma compact_segment [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "compact (closed_segment a b)"
@@ -801,8 +697,7 @@
 lemma open_segment_bound:
   assumes "x \<in> open_segment a b"
   shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
-apply (simp add: assms open_segment_bound1)
-by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
+  by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)+
 
 lemma closure_open_segment [simp]:
   "closure (open_segment a b) = (if a = b then {} else closed_segment a b)"
@@ -814,12 +709,10 @@
 next
   case False
   have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
-    apply (rule closure_injective_linear_image [symmetric])
-     apply (use False in \<open>auto intro!: injI\<close>)
-    done
+  proof (rule closure_injective_linear_image [symmetric])
+  qed (use False in \<open>auto intro!: injI\<close>)
   then have "closure
-     ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) =
-    (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
+     ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
     using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"]
     by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image)
   then show ?thesis
@@ -852,12 +745,12 @@
 lemma subset_closed_segment:
     "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
      a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
+  using closed_segment_subset convex_closed_segment ends_in_segment in_mono by blast
 
 lemma subset_co_segment:
-    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+  "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
      a \<in> open_segment c d \<and> b \<in> open_segment c d"
-using closed_segment_subset by blast
+  using closed_segment_subset by blast
 
 lemma subset_open_segment:
   fixes a :: "'a::euclidean_space"
@@ -890,8 +783,7 @@
         have "\<not> p \<le> 0" "\<not> q \<le> 0"
           using p q not_less by blast+
         then show ?thesis
-          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
-                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
+          by (smt (verit) \<open>ua \<noteq> ub\<close> mult_cancel_left1 mult_left_le uab(2) uab(4))
       qed
       then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
         by (metis diff_add_cancel diff_gt_0_iff_gt)
@@ -925,10 +817,14 @@
 lemma subset_oc_segment:
   fixes a :: "'a::euclidean_space"
   shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
-         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-  apply (rule iffI)
-   apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment)
-  by (meson dual_order.trans segment_open_subset_closed subset_open_segment)
+         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d" 
+    (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (meson dual_order.trans segment_open_subset_closed subset_open_segment)
+qed
 
 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
 
@@ -1048,12 +944,12 @@
 lemma betweenI:
   assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
   shows "between (a, b) x"
-using assms unfolding between_def closed_segment_def by auto
+  using assms unfolding between_def closed_segment_def by auto
 
 lemma betweenE:
   assumes "between (a, b) x"
   obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
-using assms unfolding between_def closed_segment_def by auto
+  using assms unfolding between_def closed_segment_def by auto
 
 lemma between_implies_scaled_diff:
   assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
@@ -1064,11 +960,7 @@
   from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T"
     by (metis add.commute betweenE eq_diff_eq)
   have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
-  proof -
-    from X Y have "X - Y =  u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
-    also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
-    finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
-  qed
+    by (simp add: X Y scaleR_left.diff scaleR_right_diff_distrib)
   moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
     by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
   moreover note \<open>S \<noteq> Y\<close>
@@ -1154,17 +1046,17 @@
   by (auto simp: between_def)
 
 lemma between_commute:
-   "between (a,b) = between (b,a)"
-by (auto simp: between_def closed_segment_commute)
+  "between (a,b) = between (b,a)"
+  by (auto simp: between_def closed_segment_commute)
 
 lemma between_antisym:
   fixes a :: "'a :: euclidean_space"
   shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
-by (auto simp: between dist_commute)
+  by (auto simp: between dist_commute)
 
 lemma between_trans:
-    fixes a :: "'a :: euclidean_space"
-    shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
+  fixes a :: "'a :: euclidean_space"
+  shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
   using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
   by (auto simp: between dist_commute)
 
@@ -1178,7 +1070,7 @@
   assumes "between (A, B) X"
   assumes "between (A, B) Y"
   shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
-using assms by (auto simp add: between)
+  using assms by (auto simp add: between)
 
 lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
   by (auto simp: between_def)
@@ -1191,7 +1083,7 @@
 lemma between_scaleR_lift [simp]:
   fixes v :: "'a::euclidean_space"
   shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c"
-  by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])
+  by (simp add: between dist_norm flip: scaleR_left_diff_distrib distrib_right)
 
 lemma between_1:
   fixes x::real