diff -r c9ffd9cf58db -r 23f819af2d9f src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Tue Jan 03 11:30:37 2023 +0000
+++ b/src/HOL/Analysis/Polytope.thy	Tue Jan 03 17:02:41 2023 +0000
@@ -474,10 +474,7 @@
     using order.trans by fastforce
 next
   case False
-  then show ?thesis
-    apply simp
-    apply (erule ex_forward)
-    by blast
+  then show ?thesis by fastforce
 qed
 
 lemma faces_of_translation:
@@ -661,23 +658,16 @@
 
 lemma exposed_face_of:
     "T exposed_face_of S \<longleftrightarrow>
-     T face_of S \<and>
-     (T = {} \<or> T = S \<or>
+     T face_of S \<and> (T = {} \<or> T = S \<or>
       (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
-proof (cases "T = {}")
-  case False
-  show ?thesis
-  proof (cases "T = S")
-    case True then show ?thesis
-      by (simp add: face_of_refl_eq)
-  next
-    case False
-    with \<open>T \<noteq> {}\<close> show ?thesis
-      apply (auto simp: exposed_face_of_def)
-      apply (metis inner_zero_left)
-      done
-  qed
-qed auto
+     (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (smt (verit) Collect_cong exposed_face_of_def hyperplane_eq_empty inf.absorb_iff1
+                    inf_bot_right inner_zero_left)
+  show "?rhs \<Longrightarrow> ?lhs"
+    using exposed_face_of_def face_of_imp_convex by fastforce
+qed
 
 lemma exposed_face_of_Int_supporting_hyperplane_le:
    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
@@ -780,10 +770,7 @@
     proof -
       have "\<And>x y. \<lbrakk>z = u \<bullet> (x + y); x \<in> S; y \<in> T\<rbrakk>
            \<Longrightarrow> u \<bullet> x = u \<bullet> a0 \<and> u \<bullet> y = u \<bullet> b0"
-        using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
-        apply (simp add: inner_right_distrib)
-        apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
-        done
+        by (smt (verit, best) z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close> inner_right_distrib lez)
       then show ?thesis
         using feq by blast
     qed
@@ -815,18 +802,18 @@
       then show ?thesis
       proof
         assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
-       then show ?thesis
-         apply (rule_tac x="0" in exI)
-         apply (rule_tac x="1" in exI)
-         using hull_subset by fastforce
+        then show ?thesis
+          apply (rule_tac x="0" in exI)
+          apply (rule_tac x="1" in exI)
+          using hull_subset by fastforce
+      next
+        assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
+        then show ?thesis
+          apply (rule_tac x="0" in exI)
+          apply (rule_tac x="0" in exI)
+          using Ssub hull_subset by fastforce
+      qed
     next
-      assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
-      then show ?thesis
-         apply (rule_tac x="0" in exI)
-         apply (rule_tac x="0" in exI)
-        using Ssub hull_subset by fastforce
-    qed
-  next
     case False
     then obtain a' b' where "a' \<noteq> 0" 
       and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
@@ -1472,9 +1459,8 @@
   have "\<not> affine_dependent c"
     using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
   with affs have "card (S - c) = 1"
-    apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
-    by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
-                add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
+    by (smt (verit) \<open>c \<subseteq> S\<close> aff_dim_affine_independent aff_independent_finite assms card_Diff_subset 
+        card_mono of_nat_diff of_nat_eq_1_iff)
   then obtain u where u: "u \<in> S - c"
     by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
                 card_Diff_subset subsetI subset_antisym zero_neq_one)
@@ -3361,11 +3347,9 @@
                 ultimately show "convex hull (J - {?z}) \<in> \<U> \<inter> Pow (rel_frontier C)" by auto
                 let ?F = "convex hull insert ?z (convex hull (J - {?z}))"
                 have "F \<subseteq> ?F"
-                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
-                  by (metis True subsetD hull_mono hull_subset subset_insert_iff)
+                  by (simp add: \<open>F = convex hull J\<close> hull_mono hull_subset subset_insert_iff)
                 moreover have "?F \<subseteq> F"
-                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
-                  by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff)
+                  by (metis True \<open>F = convex hull J\<close> hull_insert insert_Diff set_eq_subset)
                 ultimately
                 show "F \<in> {?F}" by auto
               qed