# HG changeset patch
# User paulson
# Date 1690307554 -3600
# Node ID 0bd81d52859822f920d785a67286282d18c6ef19
# Parent  127e4e952446e10db2536594c0129eea5809435d# Parent  51b8f6a19978c84cd2a61b25282a192d9fdefcd6
merged

diff -r 127e4e952446 -r 0bd81d528598 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jul 25 15:04:17 2023 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jul 25 18:52:34 2023 +0100
@@ -22,40 +22,39 @@
 
 lemma retract_of_contractible:
   assumes "contractible T" "S retract_of T"
-    shows "contractible S"
-using assms
-apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset)
-apply (rule_tac x="r a" in exI)
-apply (rule_tac x="r \<circ> h" in exI)
-apply (intro conjI continuous_intros continuous_on_compose)
-apply (erule continuous_on_subset | force)+
-done
+  shows "contractible S"
+  using assms
+  apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with image_subset_iff_funcset)
+  apply (rule_tac x="r a" in exI)
+  apply (rule_tac x="r \<circ> h" in exI)
+  apply (intro conjI continuous_intros continuous_on_compose)
+      apply (erule continuous_on_subset | force)+
+  done
 
 lemma retract_of_path_connected:
     "\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
   by (metis path_connected_continuous_image retract_of_def retraction)
 
 lemma retract_of_simply_connected:
-    "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
-apply (simp add: retract_of_def retraction_def, clarify)
-apply (rule simply_connected_retraction_gen)
-apply (force elim!: continuous_on_subset)+
-done
+  "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
+  apply (simp add: retract_of_def retraction_def Pi_iff, clarify)
+  apply (rule simply_connected_retraction_gen)
+       apply (force elim!: continuous_on_subset)+
+  done
 
 lemma retract_of_homotopically_trivial:
   assumes ts: "T retract_of S"
-      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
-                       continuous_on U g; g ` U \<subseteq> S\<rbrakk>
+      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S;
+                       continuous_on U g; g \<in> U \<rightarrow> S\<rbrakk>
                        \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
-      and "continuous_on U f" "f ` U \<subseteq> T"
-      and "continuous_on U g" "g ` U \<subseteq> T"
+      and "continuous_on U f" "f \<in> U \<rightarrow> T"
+      and "continuous_on U g" "g \<in> U \<rightarrow> T"
     shows "homotopic_with_canon (\<lambda>x. True) U T f g"
 proof -
-  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
+  obtain r where "r \<in> S \<rightarrow> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
     using ts by (auto simp: retract_of_def retraction)
   then obtain k where "Retracts S r T k"
-    unfolding Retracts_def
-    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
+    unfolding Retracts_def using continuous_on_id by blast
   then show ?thesis
     apply (rule Retracts.homotopically_trivial_retraction_gen)
     using assms
@@ -65,16 +64,15 @@
 
 lemma retract_of_homotopically_trivial_null:
   assumes ts: "T retract_of S"
-      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
+      and hom: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S\<rbrakk>
                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
-      and "continuous_on U f" "f ` U \<subseteq> T"
+      and "continuous_on U f" "f \<in> U \<rightarrow> T"
   obtains c where "homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
 proof -
-  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
+  obtain r where "r \<in> S \<rightarrow> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
     using ts by (auto simp: retract_of_def retraction)
   then obtain k where "Retracts S r T k"
-    unfolding Retracts_def
-    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
+    unfolding Retracts_def by fastforce
   then show ?thesis
     apply (rule Retracts.homotopically_trivial_retraction_null_gen)
     apply (rule TrueI refl assms that | assumption)+
@@ -92,25 +90,24 @@
   by (metis locally_compact_closedin closedin_retract)
 
 lemma homotopic_into_retract:
-   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
+   "\<lbrakk>f \<in> S \<rightarrow> T; g \<in> S \<rightarrow> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
         \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
-apply (subst (asm) homotopic_with_def)
-apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
-apply (rule_tac x="r \<circ> h" in exI)
-apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
-done
+  apply (subst (asm) homotopic_with_def)
+  apply (simp add: homotopic_with retract_of_def retraction_def Pi_iff, clarify)
+  apply (rule_tac x="r \<circ> h" in exI)
+  by (smt (verit, ccfv_SIG) comp_def continuous_on_compose continuous_on_subset image_subset_iff)
 
 lemma retract_of_locally_connected:
   assumes "locally connected T" "S retract_of T"
   shows "locally connected S"
   using assms
-  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
+  by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)
 
 lemma retract_of_locally_path_connected:
   assumes "locally path_connected T" "S retract_of T"
   shows "locally path_connected S"
   using assms
-  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
+  by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)
 
 text \<open>A few simple lemmas about deformation retracts\<close>
 
@@ -133,7 +130,7 @@
 lemma deformation_retract:
   fixes S :: "'a::euclidean_space set"
     shows "(\<exists>r. homotopic_with_canon (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
-           T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
+           T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f \<in> S \<rightarrow> T)"
     (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -147,7 +144,7 @@
      apply (rule homotopic_with_trans, assumption)
      apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
         apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
-         apply (auto simp: homotopic_with_sym)
+         apply (auto simp: homotopic_with_sym Pi_iff)
     done
 qed
 
@@ -161,10 +158,10 @@
   moreover have "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
       using assms
       by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
-  moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
+  moreover have "(\<lambda>x. a) \<in> S \<rightarrow> {a}"
     by (simp add: image_subsetI)
   ultimately show ?thesis
-    using that deformation_retract  by metis
+    by (metis that deformation_retract)
 qed
 
 
diff -r 127e4e952446 -r 0bd81d528598 src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Tue Jul 25 15:04:17 2023 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Tue Jul 25 18:52:34 2023 +0100
@@ -17,9 +17,8 @@
 lemma interval_bij_affine:
   "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
     (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
-  by (auto simp add: interval_bij_def sum.distrib [symmetric] scaleR_add_left [symmetric]
-    fun_eq_iff intro!: sum.cong)
-    (simp add: algebra_simps diff_divide_distrib [symmetric])
+  by (simp add: interval_bij_def algebra_simps add_divide_distrib diff_divide_distrib flip: sum.distrib scaleR_add_left)
+
 
 lemma continuous_interval_bij:
   fixes a b :: "'a::euclidean_space"
@@ -27,38 +26,22 @@
   by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)
 
 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
-  apply(rule continuous_at_imp_continuous_on)
-  apply (rule, rule continuous_interval_bij)
-  done
+  by (metis continuous_at_imp_continuous_on continuous_interval_bij)
 
 lemma in_interval_interval_bij:
   fixes a b u v x :: "'a::euclidean_space"
   assumes "x \<in> cbox a b"
     and "cbox u v \<noteq> {}"
   shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
-  apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
-  apply safe
 proof -
-  fix i :: 'a
-  assume i: "i \<in> Basis"
-  have "cbox a b \<noteq> {}"
-    using assms by auto
-  with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
-    using assms(2) by (auto simp add: box_eq_empty)
-  have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
-    using assms(1)[unfolded mem_box] using i by auto
-  have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
-    using * x by auto
-  then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
-    using * by auto
-  have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
-    apply (rule mult_right_mono)
-    unfolding divide_le_eq_1
-    using * x
-    apply auto
-    done
-  then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
-    using * by auto
+  have "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
+    by (smt (verit) assms box_ne_empty(1) divide_nonneg_nonneg mem_box(2) mult_nonneg_nonneg)
+  moreover
+  have "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
+    apply (simp add: divide_simps algebra_simps)
+    by (smt (verit, best) assms box_ne_empty(1) left_diff_distrib mem_box(2) mult.commute mult_left_mono)
+  ultimately show ?thesis
+    by (force simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis)
 qed
 
 lemma interval_bij_bij:
@@ -107,9 +90,9 @@
     where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
   define negatex :: "real^2 \<Rightarrow> real^2"
     where "negatex x = (vector [-(x$1), x$2])" for x
-  have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
+  have inf_nega: "\<And>z::real^2. infnorm (negatex z) = infnorm z"
     unfolding negatex_def infnorm_2 vector_2 by auto
-  have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
+  have inf_eq1: "\<And>z. z \<noteq> 0 \<Longrightarrow> infnorm (sqprojection z) = 1"
     unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR]
     by (simp add: real_abs_infnorm infnorm_eq_0)
   let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
@@ -128,75 +111,59 @@
         "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
       unfolding image_iff ..
     then have "x \<noteq> 0"
-      using as[of "w$1" "w$2"]
-      unfolding mem_box_cart atLeastAtMost_iff
-      by auto
+      using as[of "w$1" "w$2"] by (auto simp: mem_box_cart atLeastAtMost_iff)
   } note x0 = this
-  have 1: "box (- 1) (1::real^2) \<noteq> {}"
-    unfolding interval_eq_empty_cart by auto
-  have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
-    for i x y c
-    using exhaust_2 [of i] by (auto simp: negatex_def)
-  then have "bounded_linear negatex"
-    by (simp add: bounded_linearI' vec_eq_iff)
-  then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
-    apply (intro continuous_intros continuous_on_component)
-    unfolding * sqprojection_def
-    apply (intro assms continuous_intros)+
-     apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
-    done
-  have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
-    unfolding subset_eq
-  proof (rule, goal_cases)
-    case (1 x)
-    then obtain y :: "real^2" where y:
-        "y \<in> cbox (- 1) 1"
-        "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
-      unfolding image_iff ..
-    have "?F y \<noteq> 0"
-      by (rule x0) (use y in auto)
-    then have *: "infnorm (sqprojection (?F y)) = 1"
-      unfolding y o_def
-      by - (rule lem2[rule_format])
-    have inf1: "infnorm x = 1"
-      unfolding *[symmetric] y o_def
-      by (rule lem1[rule_format])
-    show "x \<in> cbox (-1) 1"
-      unfolding mem_box_cart interval_cbox_cart infnorm_2
-    proof 
-      fix i
-      show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
-        using exhaust_2 [of i] inf1 by (auto simp: infnorm_2)
-    qed
-  qed
+  let ?CB11 = "cbox (- 1) (1::real^2)"
   obtain x :: "real^2" where x:
       "x \<in> cbox (- 1) 1"
       "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
-    apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
-    apply (rule compact_cbox convex_box)+
-    unfolding interior_cbox image_subset_iff_funcset [symmetric]
-       apply (rule 1 2 3)+
-    apply blast
-    done
+  proof (rule brouwer_weak[of ?CB11 "negatex \<circ> sqprojection \<circ> ?F"])
+    show "compact ?CB11" "convex ?CB11"
+      by (rule compact_cbox convex_box)+
+    have "box (- 1) (1::real^2) \<noteq> {}"
+      unfolding interval_eq_empty_cart by auto
+    then show "interior ?CB11 \<noteq> {}"
+      by simp
+    have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
+      for i x y c
+      using exhaust_2 [of i] by (auto simp: negatex_def)
+    then have "bounded_linear negatex"
+      by (simp add: bounded_linearI' vec_eq_iff)
+    then show "continuous_on ?CB11 (negatex \<circ> sqprojection \<circ> ?F)"
+      unfolding sqprojection_def
+      apply (intro continuous_intros continuous_on_component | use * assms in presburger)+
+       apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
+      done
+    have "(negatex \<circ> sqprojection \<circ> ?F) ` ?CB11 \<subseteq> ?CB11"
+    proof clarsimp
+      fix y :: "real^2" 
+      assume y: "y \<in> ?CB11"
+      have "?F y \<noteq> 0"
+        by (rule x0) (use y in auto)
+      then have *: "infnorm (sqprojection (?F y)) = 1"
+        using inf_eq1 by blast
+      show "negatex (sqprojection (f (y $ 1) - g (y $ 2))) \<in> cbox (-1) 1"
+        unfolding mem_box_cart interval_cbox_cart infnorm_2
+        by (smt (verit, del_insts) "*" component_le_infnorm_cart inf_nega neg_one_index o_apply one_index)
+    qed
+    then show "negatex \<circ> sqprojection \<circ> ?F \<in> ?CB11 \<rightarrow> ?CB11"
+      by blast
+  qed
   have "?F x \<noteq> 0"
     by (rule x0) (use x in auto)
   then have *: "infnorm (sqprojection (?F x)) = 1"
-    unfolding o_def
-    by (rule lem2[rule_format])
+    using inf_eq1 by blast
   have nx: "infnorm x = 1"
-    apply (subst x(2)[symmetric])
-    unfolding *[symmetric] o_def
-    apply (rule lem1[rule_format])
-    done
+    by (metis (no_types, lifting) "*" inf_nega o_apply x(2))
   have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for x i
   proof -
-    have "inverse (infnorm x) > 0"
+    have *: "inverse (infnorm x) > 0"
       by (simp add: infnorm_pos_lt that)
     then show "(0 < sqprojection x $ i) = (0 < x $ i)"
-      and "(sqprojection x $ i < 0) = (x $ i < 0)"
-      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
-      unfolding zero_less_mult_iff mult_less_0_iff
-      by (auto simp add: field_simps)
+      by (simp add: sqprojection_def zero_less_mult_iff)
+    show "(sqprojection x $ i < 0) = (x $ i < 0)"
+      unfolding sqprojection_def
+        by (metis * pos_less_divideR_eq scaleR_zero_right vector_scaleR_component)
   qed
   have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
     using x(1) unfolding mem_box_cart by auto
@@ -210,8 +177,7 @@
     then have *: "f (x $ 1) $ 1 = - 1"
       using assms(5) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
-      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
-      by (auto simp: negatex_def 1)
+      by (smt (verit) "1" negatex_def o_apply vector_2(1) x(2))
     moreover
     from x1 have "g (x $ 2) \<in> cbox (-1) 1"
       using assms(2) by blast
@@ -223,8 +189,7 @@
     then have *: "f (x $ 1) $ 1 = 1"
       using assms(6) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
-      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2
-      by (auto simp: negatex_def)
+      by (smt (verit) "2" negatex_def o_apply vector_2(1) x(2) zero_less_one)
     moreover have "g (x $ 2) \<in> cbox (-1) 1"
       using assms(2) x1 by blast
     ultimately show False
@@ -234,26 +199,23 @@
     case 3
     then have *: "g (x $ 2) $ 2 = - 1"
       using assms(7) by auto
-    have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
-      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def)
-    moreover
-    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
+    moreover have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
+      by (smt (verit, ccfv_SIG) "3" negatex_def o_apply vector_2(2) x(2))
+    moreover from x1 have "f (x $ 1) \<in> cbox (-1) 1"
       using assms(1) by blast
     ultimately show False
-      unfolding iff[OF nz] vector_component_simps * mem_box_cart
-      by (erule_tac x=2 in allE) auto
+      by (smt (verit, del_insts) iff(2) mem_box_cart(2) neg_one_index nz vector_minus_component)
   next
     case 4
     then have *: "g (x $ 2) $ 2 = 1"
       using assms(8) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
-      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def)
+      by (smt (verit, best) "4" negatex_def o_apply vector_2(2) x(2))
     moreover
     from x1 have "f (x $ 1) \<in> cbox (-1) 1"
       using assms(1) by blast
     ultimately show False
-      unfolding iff[OF nz] vector_component_simps * mem_box_cart
-      by (erule_tac x=2 in allE) auto
+      by (smt (verit) "*" iff(1) mem_box_cart(2) nz one_index vector_minus_component)
   qed 
 qed
 
@@ -269,7 +231,7 @@
     and "(pathfinish g)$2 = 1"
   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
 proof -
-  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
+  note assms = assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
   define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
   have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
     unfolding iscale_def by auto
@@ -279,38 +241,27 @@
       using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
     have *: "continuous_on {- 1..1} iscale"
       unfolding iscale_def by (rule continuous_intros)+
-    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
-      apply -
-      apply (rule_tac[!] continuous_on_compose[OF *])
-      apply (rule_tac[!] continuous_on_subset[OF _ isc])
-      apply (rule assms)+
-      done
+    show "continuous_on {- 1..1} (f \<circ> iscale)"
+      using "*" assms(1) continuous_on_compose continuous_on_subset isc by blast
+    show "continuous_on {- 1..1} (g \<circ> iscale)"
+      by (meson "*" assms(2) continuous_on_compose continuous_on_subset isc)
     have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
       unfolding vec_eq_iff by auto
     show "(f \<circ> iscale) (- 1) $ 1 = - 1"
       and "(f \<circ> iscale) 1 $ 1 = 1"
       and "(g \<circ> iscale) (- 1) $ 2 = -1"
       and "(g \<circ> iscale) 1 $ 2 = 1"
-      unfolding o_def iscale_def
-      using assms
-      by (auto simp add: *)
+      unfolding o_def iscale_def using assms by (auto simp add: *)
   qed
-  then obtain s t where st:
-      "s \<in> {- 1..1}"
-      "t \<in> {- 1..1}"
-      "(f \<circ> iscale) s = (g \<circ> iscale) t"
+  then obtain s t where st: "s \<in> {- 1..1}" "t \<in> {- 1..1}" "(f \<circ> iscale) s = (g \<circ> iscale) t"
     by auto
   show thesis
-    apply (rule_tac z = "f (iscale s)" in that)
-    using st
-    unfolding o_def path_image_def image_iff
-    apply -
-    apply (rule_tac x="iscale s" in bexI)
-    prefer 3
-    apply (rule_tac x="iscale t" in bexI)
-    using isc[unfolded subset_eq, rule_format]
-    apply auto
-    done
+  proof
+    show "f (iscale s) \<in> path_image f"
+      by (metis image_eqI image_subset_iff isc path_image_def st(1))
+    show "f (iscale s) \<in> path_image g"
+      by (metis comp_def image_eqI image_subset_iff isc path_image_def st(2) st(3))
+  qed
 qed
 
 theorem fashoda:
@@ -339,66 +290,39 @@
 next
   assume as: "a$1 = b$1"
   have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
-    apply (rule connected_ivt_component_cart)
-    apply (rule connected_path_image assms)+
-    apply (rule pathstart_in_path_image)
-    apply (rule pathfinish_in_path_image)
-    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
-    unfolding pathstart_def
-    apply (auto simp add: less_eq_vec_def mem_box_cart)
-    done
+  proof (rule connected_ivt_component_cart)
+    show "pathstart g $ 2 \<le> pathstart f $ 2"
+      by (metis assms(3) assms(7) mem_box_cart(2) pathstart_in_path_image subset_iff)
+    show "pathstart f $ 2 \<le> pathfinish g $ 2"
+      by (metis assms(3) assms(8) in_mono mem_box_cart(2) pathstart_in_path_image)
+    show "connected (path_image g)"
+      using assms(2) by blast
+  qed (auto simp: path_defs)
   then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
   have "z \<in> cbox a b"
-    using z(1) assms(4)
-    unfolding path_image_def
-    by blast
+    using assms(4) z(1) by blast
   then have "z = f 0"
-    unfolding vec_eq_iff forall_2
-    unfolding z(2) pathstart_def
-    using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
-    unfolding mem_box_cart
-    apply (erule_tac x=1 in allE)
-    using as
-    apply auto
-    done
+    by (smt (verit) as assms(5) exhaust_2 mem_box_cart(2) nle_le pathstart_def vec_eq_iff z(2))
   then show thesis
-    apply -
-    apply (rule that[OF _ z(1)])
-    unfolding path_image_def
-    apply auto
-    done
+    by (metis path_defs(2) pathstart_in_path_image that z(1))
 next
   assume as: "a$2 = b$2"
   have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
-    apply (rule connected_ivt_component_cart)
-    apply (rule connected_path_image assms)+
-    apply (rule pathstart_in_path_image)
-    apply (rule pathfinish_in_path_image)
-    unfolding assms
-    using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
-    unfolding pathstart_def
-    apply (auto simp add: less_eq_vec_def mem_box_cart)
-    done
+  proof (rule connected_ivt_component_cart)
+    show "pathstart f $ 1 \<le> pathstart g $ 1"
+      using assms(4) assms(5) mem_box_cart(2) by fastforce
+    show "pathstart g $ 1 \<le> pathfinish f $ 1"
+      using assms(4) assms(6) mem_box_cart(2) pathstart_in_path_image by fastforce
+    show "connected (path_image f)"
+      by (simp add: assms(1) connected_path_image)
+  qed (auto simp: path_defs)
   then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
   have "z \<in> cbox a b"
-    using z(1) assms(3)
-    unfolding path_image_def
-    by blast
+    using assms(3) z(1) by auto
   then have "z = g 0"
-    unfolding vec_eq_iff forall_2
-    unfolding z(2) pathstart_def
-    using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
-    unfolding mem_box_cart
-    apply (erule_tac x=2 in allE)
-    using as
-    apply auto
-    done
+    by (smt (verit) as assms(7) exhaust_2 mem_box_cart(2) pathstart_def vec_eq_iff z(2))
   then show thesis
-    apply -
-    apply (rule that[OF z(1)])
-    unfolding path_image_def
-    apply auto
-    done
+    by (metis path_defs(2) pathstart_in_path_image that z(1))
 next
   assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
   have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
@@ -406,61 +330,30 @@
   obtain z :: "real^2" where z:
       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
-    apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
-    unfolding path_def path_image_def pathstart_def pathfinish_def
-    apply (rule_tac[1-2] continuous_on_compose)
-    apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
-    unfolding subset_eq
-    apply(rule_tac[1-2] ballI)
-  proof -
-    fix x
-    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
-    then obtain y where y:
-        "y \<in> {0..1}"
-        "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
-      unfolding image_iff ..
-    show "x \<in> cbox (- 1) 1"
-      unfolding y o_def
-      apply (rule in_interval_interval_bij)
-      using y(1)
-      using assms(3)[unfolded path_image_def subset_eq] int_nem
-      apply auto
-      done
-  next
-    fix x
-    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
-    then obtain y where y:
-        "y \<in> {0..1}"
-        "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
-      unfolding image_iff ..
-    show "x \<in> cbox (- 1) 1"
-      unfolding y o_def
-      apply (rule in_interval_interval_bij)
-      using y(1)
-      using assms(4)[unfolded path_image_def subset_eq] int_nem
-      apply auto
-      done
-  next
-    show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
-      and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
-      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
-      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
+  proof (rule fashoda_unit_path)
+    show "path (interval_bij (a, b) (- 1, 1) \<circ> f)"
+      by (meson assms(1) continuous_on_interval_bij path_continuous_image)
+    show "path (interval_bij (a, b) (- 1, 1) \<circ> g)"
+      by (meson assms(2) continuous_on_interval_bij path_continuous_image)
+    show "path_image (interval_bij (a, b) (- 1, 1) \<circ> f) \<subseteq> cbox (- 1) 1"
+      using assms(3)
+      by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq)
+    show "path_image (interval_bij (a, b) (- 1, 1) \<circ> g) \<subseteq> cbox (- 1) 1"
+      using assms(4)
+      by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq)
+    show "pathstart (interval_bij (a, b) (- 1, 1) \<circ> f) $ 1 = - 1"
+         "pathfinish (interval_bij (a, b) (- 1, 1) \<circ> f) $ 1 = 1"
+         "pathstart (interval_bij (a, b) (- 1, 1) \<circ> g) $ 2 = - 1"
+         "pathfinish (interval_bij (a, b) (- 1, 1) \<circ> g) $ 2 = 1"
       using assms as
       by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
          (simp_all add: inner_axis)
-  qed
-  from z(1) obtain zf where zf:
-      "zf \<in> {0..1}"
-      "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
-    unfolding image_iff ..
-  from z(2) obtain zg where zg:
-      "zg \<in> {0..1}"
-      "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
-    unfolding image_iff ..
+  qed (auto simp: path_defs)
+  then obtain zf zg where zf: "zf \<in> {0..1}" "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf" 
+                    and zg: "zg \<in> {0..1}" "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
+    by blast
   have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
-    unfolding forall_2
-    using as
-    by auto
+    unfolding forall_2 using as by auto
   show thesis
   proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
     show "interval_bij (- 1, 1) (a, b) z \<in> path_image f"
@@ -493,62 +386,43 @@
     then obtain u where u:
         "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
         "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
-        "0 \<le> u"
-        "u \<le> 1"
+        "0 \<le> u" "u \<le> 1"
       by blast
     { fix b a
       assume "b + u * a > a + u * b"
       then have "(1 - u) * b > (1 - u) * a"
         by (auto simp add:field_simps)
       then have "b \<ge> a"
-        apply (drule_tac mult_left_less_imp_less)
-        using u
-        apply auto
-        done
+        using not_less_iff_gr_or_eq u(4) by fastforce
       then have "u * a \<le> u * b"
-        apply -
-        apply (rule mult_left_mono[OF _ u(3)])
-        using u(3-4)
-        apply (auto simp add: field_simps)
-        done
-    } note * = this
-    {
-      fix a b
+        by (simp add: mult_left_mono u(3))
+    } 
+    moreover
+    { fix a b
       assume "u * b > u * a"
       then have "(1 - u) * a \<le> (1 - u) * b"
-        apply -
-        apply (rule mult_left_mono)
-        apply (drule mult_left_less_imp_less)
-        using u
-        apply auto
-        done
+        using less_eq_real_def u(3) u(4) by force
       then have "a + u * b \<le> b + u * a"
         by (auto simp add: field_simps)
-    } note ** = this
-    then show ?R
-      unfolding u assms
-      using u
-      by (auto simp add:field_simps not_le intro: * **)
+    } ultimately show ?R
+      by (force simp add: u assms field_simps not_le)
   }
   {
     assume ?R
     then show ?L
     proof (cases "x$2 = b$2")
       case True
-      then show ?L
-        apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
-        unfolding assms True using \<open>?R\<close> apply (auto simp add: field_simps)
-        done
+      with \<open>?R\<close> show ?L
+        by (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) (auto simp add: field_simps)
     next
       case False
-      then show ?L
-        apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
-        unfolding assms using \<open>?R\<close> apply (auto simp add: field_simps)
-        done
+      with \<open>?R\<close> show ?L
+          by (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) (auto simp add: field_simps)
     qed
   }
 qed
 
+text \<open>Essentially duplicate proof that could be done by swapping co-ordinates\<close>
 lemma segment_horizontal:
   fixes a :: "real^2"
   assumes "a$2 = b$2"
@@ -569,63 +443,38 @@
     then obtain u where u:
         "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
         "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
-        "0 \<le> u"
-        "u \<le> 1"
+        "0 \<le> u" "u \<le> 1"
       by blast
-    {
-      fix b a
+    { fix b a
       assume "b + u * a > a + u * b"
       then have "(1 - u) * b > (1 - u) * a"
         by (auto simp add: field_simps)
       then have "b \<ge> a"
-        apply (drule_tac mult_left_less_imp_less)
-        using u
-        apply auto
-        done
+        by (smt (verit, best) mult_left_mono u(4))
       then have "u * a \<le> u * b"
-        apply -
-        apply (rule mult_left_mono[OF _ u(3)])
-        using u(3-4)
-        apply (auto simp add: field_simps)
-        done
-    } note * = this
-    {
-      fix a b
+        by (simp add: mult_left_mono u(3))
+    } 
+    moreover
+    { fix a b
       assume "u * b > u * a"
       then have "(1 - u) * a \<le> (1 - u) * b"
-        apply -
-        apply (rule mult_left_mono)
-        apply (drule mult_left_less_imp_less)
-        using u
-        apply auto
-        done
+        using less_eq_real_def u(3) u(4) by force
       then have "a + u * b \<le> b + u * a"
         by (auto simp add: field_simps)
-    } note ** = this
-    then show ?R
-      unfolding u assms
-      using u
-      by (auto simp add: field_simps not_le intro: * **)
+    } 
+    ultimately show ?R
+      by (force simp add: u assms field_simps not_le intro: )
   }
-  {
-    assume ?R
+  { assume ?R
     then show ?L
     proof (cases "x$1 = b$1")
       case True
-      then show ?L
-        apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
-        unfolding assms True
-        using \<open>?R\<close>
-        apply (auto simp add: field_simps)
-        done
+      with \<open>?R\<close> show ?L
+        by (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) (auto simp add: field_simps)
     next
       case False
-      then show ?L
-        apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
-        unfolding assms
-        using \<open>?R\<close>
-        apply (auto simp add: field_simps)
-        done
+      with \<open>?R\<close> show ?L
+        by (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) (auto simp add: field_simps)
     qed
   }
 qed
@@ -726,9 +575,7 @@
       then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
         unfolding mem_box_cart forall_2 by auto
       then have "z$1 \<noteq> pathfinish f$1"
-        using prems(2)
-        using assms ab
-        by (auto simp add: field_simps)
+        using assms(10) assms(11) prems(2) by auto
       moreover have "pathstart f \<in> cbox a b"
         using assms(3) pathstart_in_path_image[of f]
         by auto
@@ -766,7 +613,7 @@
     with z' show "z \<in> path_image f"
       using z(1)
       unfolding Un_iff mem_box_cart forall_2
-      by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
+      using assms(5) assms(6) segment_horizontal segment_vertical by auto
     have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
       z = pathstart g \<or> z = pathfinish g"
       unfolding vec_eq_iff forall_2 assms
@@ -774,7 +621,7 @@
     with z' show "z \<in> path_image g"
       using z(2)
       unfolding Un_iff mem_box_cart forall_2
-      by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
+      using assms(7) assms(8) segment_horizontal segment_vertical by auto
   qed
 qed
 
diff -r 127e4e952446 -r 0bd81d528598 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Tue Jul 25 15:04:17 2023 +0200
+++ b/src/HOL/Analysis/Homotopy.thy	Tue Jul 25 18:52:34 2023 +0100
@@ -2971,7 +2971,7 @@
   assumes S: "subspace S"
       and T: "subspace T"
       and d: "dim S \<le> dim T"
-  obtains f where "linear f" "f ` S \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+  obtains f where "linear f" "f \<in> S \<rightarrow> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
 proof -
   obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
              and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
@@ -3011,7 +3011,7 @@
       by (simp add: norm_eq_sqrt_inner)
   qed
   then show ?thesis
-    by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
+    by (meson \<open>f ` S \<subseteq> T\<close> \<open>linear f\<close> image_subset_iff_funcset that)
 qed
 
 proposition isometries_subspaces:
@@ -3190,36 +3190,36 @@
   assumes conth: "continuous_on S h"
       and imh: "h ` S = t"
       and contk: "continuous_on t k"
-      and imk: "k ` t \<subseteq> S"
+      and imk: "k \<in> t \<rightarrow> S"
       and idhk: "\<And>y. y \<in> t \<Longrightarrow> h(k y) = y"
 
 begin
 
 lemma homotopically_trivial_retraction_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
-      and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f;
-                       continuous_on U g; g ` U \<subseteq> S; P g\<rbrakk>
+      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f;
+                       continuous_on U g; g \<in> U \<rightarrow> S; P g\<rbrakk>
                        \<Longrightarrow> homotopic_with_canon P U S f g"
-      and contf: "continuous_on U f" and imf: "f ` U \<subseteq> t" and Qf: "Q f"
-      and contg: "continuous_on U g" and img: "g ` U \<subseteq> t" and Qg: "Q g"
+      and contf: "continuous_on U f" and imf: "f \<in> U \<rightarrow> t" and Qf: "Q f"
+      and contg: "continuous_on U g" and img: "g \<in> U \<rightarrow> t" and Qg: "Q g"
     shows "homotopic_with_canon Q U t f g"
 proof -
   have "continuous_on U (k \<circ> f)"
-    using contf continuous_on_compose continuous_on_subset contk imf by blast
+    by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf)
   moreover have "(k \<circ> f) ` U \<subseteq> S"
     using imf imk by fastforce
   moreover have "P (k \<circ> f)"
     by (simp add: P Qf contf imf)
   moreover have "continuous_on U (k \<circ> g)"
-    using contg continuous_on_compose continuous_on_subset contk img by blast
+    by (meson contg continuous_on_compose continuous_on_subset contk funcset_image img)
   moreover have "(k \<circ> g) ` U \<subseteq> S"
     using img imk by fastforce
   moreover have "P (k \<circ> g)"
     by (simp add: P Qg contg img)
   ultimately have "homotopic_with_canon P U S (k \<circ> f) (k \<circ> g)"
-    by (rule hom)
+    by (simp add: hom image_subset_iff)
   then have "homotopic_with_canon Q U t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
     apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
     using Q conth imh by force+
@@ -3228,23 +3228,23 @@
     show "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
       using Qeq topspace_euclidean_subtopology by blast
     show "\<And>x. x \<in> U \<Longrightarrow> f x = h (k (f x))" "\<And>x. x \<in> U \<Longrightarrow> g x = h (k (g x))"
-      using idhk imf img by auto
+      using idhk imf img by fastforce+
   qed 
 qed
 
 lemma homotopically_trivial_retraction_null_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
-      and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk>
+      and hom: "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S; P f\<rbrakk>
                      \<Longrightarrow> \<exists>c. homotopic_with_canon P U S f (\<lambda>x. c)"
-      and contf: "continuous_on U f" and imf:"f ` U \<subseteq> t" and Qf: "Q f"
+      and contf: "continuous_on U f" and imf:"f \<in> U \<rightarrow> t" and Qf: "Q f"
   obtains c where "homotopic_with_canon Q U t f (\<lambda>x. c)"
 proof -
   have feq: "\<And>x. x \<in> U \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
   have "continuous_on U (k \<circ> f)"
-    using contf continuous_on_compose continuous_on_subset contk imf by blast
-  moreover have "(k \<circ> f) ` U \<subseteq> S"
+    by (meson contf continuous_on_compose continuous_on_subset contk funcset_image imf)
+  moreover have "(k \<circ> f) \<in> U \<rightarrow> S"
     using imf imk by fastforce
   moreover have "P (k \<circ> f)"
     by (simp add: P Qf contf imf)
@@ -3265,32 +3265,32 @@
 qed
 
 lemma cohomotopically_trivial_retraction_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
-      and Q: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f \<in> t \<rightarrow> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
+      and Q: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f g. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f;
-                       continuous_on S g; g ` S \<subseteq> U; P g\<rbrakk>
+      and hom: "\<And>f g. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f;
+                       continuous_on S g; g \<in> S \<rightarrow> U; P g\<rbrakk>
                        \<Longrightarrow> homotopic_with_canon P S U f g"
-      and contf: "continuous_on t f" and imf: "f ` t \<subseteq> U" and Qf: "Q f"
-      and contg: "continuous_on t g" and img: "g ` t \<subseteq> U" and Qg: "Q g"
+      and contf: "continuous_on t f" and imf: "f \<in> t \<rightarrow> U" and Qf: "Q f"
+      and contg: "continuous_on t g" and img: "g \<in> t \<rightarrow> U" and Qg: "Q g"
     shows "homotopic_with_canon Q t U f g"
 proof -
   have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
   have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
   have "continuous_on S (f \<circ> h)"
     using contf conth continuous_on_compose imh by blast
-  moreover have "(f \<circ> h) ` S \<subseteq> U"
+  moreover have "(f \<circ> h) \<in> S \<rightarrow> U"
     using imf imh by fastforce
   moreover have "P (f \<circ> h)"
     by (simp add: P Qf contf imf)
   moreover have "continuous_on S (g \<circ> h)"
     using contg continuous_on_compose continuous_on_subset conth imh by blast
-  moreover have "(g \<circ> h) ` S \<subseteq> U"
+  moreover have "(g \<circ> h) \<in> S \<rightarrow> U"
     using img imh by fastforce
   moreover have "P (g \<circ> h)"
     by (simp add: P Qg contg img)
   ultimately have "homotopic_with_canon P S U (f \<circ> h) (g \<circ> h)"
-    by (rule hom)
+    by (simp add: hom)
   then have "homotopic_with_canon Q t U (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
     apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
     using Q contk imk by force+
@@ -3303,18 +3303,18 @@
 qed
 
 lemma cohomotopically_trivial_retraction_null_gen:
-  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
-      and Q: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
+  assumes P: "\<And>f. \<lbrakk>continuous_on t f; f \<in> t \<rightarrow> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
+      and Q: "\<And>f. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f g. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk>
+      and hom: "\<And>f g. \<lbrakk>continuous_on S f; f \<in> S \<rightarrow> U; P f\<rbrakk>
                        \<Longrightarrow> \<exists>c. homotopic_with_canon P S U f (\<lambda>x. c)"
-      and contf: "continuous_on t f" and imf: "f ` t \<subseteq> U" and Qf: "Q f"
+      and contf: "continuous_on t f" and imf: "f \<in> t \<rightarrow> U" and Qf: "Q f"
   obtains c where "homotopic_with_canon Q t U f (\<lambda>x. c)"
 proof -
   have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
   have "continuous_on S (f \<circ> h)"
     using contf conth continuous_on_compose imh by blast
-  moreover have "(f \<circ> h) ` S \<subseteq> U"
+  moreover have "(f \<circ> h) \<in> S \<rightarrow> U"
     using imf imh by fastforce
   moreover have "P (f \<circ> h)"
     by (simp add: P Qf contf imf)
@@ -3335,12 +3335,12 @@
 
 lemma simply_connected_retraction_gen:
   shows "\<lbrakk>simply_connected S; continuous_on S h; h ` S = T;
-          continuous_on T k; k ` T \<subseteq> S; \<And>y. y \<in> T \<Longrightarrow> h(k y) = y\<rbrakk>
+          continuous_on T k; k \<in> T \<rightarrow> S; \<And>y. y \<in> T \<Longrightarrow> h(k y) = y\<rbrakk>
         \<Longrightarrow> simply_connected T"
 apply (simp add: simply_connected_def path_def path_image_def homotopic_loops_def, clarify)
 apply (rule Retracts.homotopically_trivial_retraction_gen
         [of S h _ k _ "\<lambda>p. pathfinish p = pathstart p"  "\<lambda>p. pathfinish p = pathstart p"])
-apply (simp_all add: Retracts_def pathfinish_def pathstart_def)
+apply (simp_all add: Retracts_def pathfinish_def pathstart_def image_subset_iff_funcset)
 done
 
 lemma homeomorphic_simply_connected:
diff -r 127e4e952446 -r 0bd81d528598 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Tue Jul 25 15:04:17 2023 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Tue Jul 25 18:52:34 2023 +0100
@@ -214,18 +214,13 @@
       fixes S :: "'a::real_normed_vector set"
       assumes "T face_of S" "T \<noteq> S"
         shows "T \<inter> interior S = {}"
-proof -
-  have "T \<inter> interior S \<subseteq> rel_interior S"
-    by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans)
-  thus ?thesis
-    by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
-qed
+  using assms face_of_disjoint_rel_interior interior_subset_rel_interior by fastforce
 
 lemma face_of_subset_rel_boundary:
   fixes S :: "'a::real_normed_vector set"
   assumes "T face_of S" "T \<noteq> S"
     shows "T \<subseteq> (S - rel_interior S)"
-by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
+  by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset subset_iff)
 
 lemma face_of_subset_rel_frontier:
     fixes S :: "'a::real_normed_vector set"
@@ -241,13 +236,8 @@
   have "aff_dim T \<le> aff_dim S"
     by (simp add: face_of_imp_subset aff_dim_subset assms)
   moreover have "aff_dim T \<noteq> aff_dim S"
-  proof (cases "T = {}")
-    case True then show ?thesis
-      by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
-  next 
-    case False then show ?thesis
-      by (smt (verit) aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex face_of_subset_rel_frontier)
-  qed
+    by (metis aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex 
+        face_of_subset_rel_frontier order_less_irrefl)
   ultimately show ?thesis
     by simp
 qed
@@ -258,7 +248,7 @@
   shows "U \<subseteq> T"
 proof (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
   show "T \<inter> rel_interior U \<noteq> {}"
-    using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T] rel_interior_subset [of U] dis \<open>U \<subseteq> S\<close> disjnt_def 
+    using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T] rel_interior_subset dis \<open>U \<subseteq> S\<close> disjnt_def 
     by fastforce
 qed
 
@@ -478,7 +468,7 @@
 qed
 
 lemma faces_of_translation:
-   "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
+   "{F. F face_of (+) a ` S} = (image ((+) a)) ` {F. F face_of S}"
 proof -
   have "\<And>F. F face_of (+) a ` S \<Longrightarrow> \<exists>G. G face_of S \<and> F = (+) a ` G"
     by (metis face_of_imp_subset face_of_translation_eq subset_imageE)
@@ -560,15 +550,12 @@
     qed
     with fst snd show ?thesis by metis
   qed
-next
-  assume ?rhs with face_of_Times show ?lhs by auto
-qed
+qed (use face_of_Times in auto)
 
 lemma face_of_Times_eq:
-    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
-    shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
-           F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
-by (auto simp: face_of_Times_decomp times_eq_iff)
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow> F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
+  by (auto simp: face_of_Times_decomp times_eq_iff)
 
 lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
 proof -
@@ -588,8 +575,7 @@
 
 lemma face_of_halfspace_le:
   fixes a :: "'n::euclidean_space"
-  shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
-         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
+  shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
      (is "?lhs = ?rhs")
 proof (cases "a = 0")
   case True then show ?thesis
@@ -623,9 +609,8 @@
 
 lemma face_of_halfspace_ge:
   fixes a :: "'n::euclidean_space"
-  shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
-         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
-using face_of_halfspace_le [of F "-a" "-b"] by simp
+  shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
+  using face_of_halfspace_le [of F "-a" "-b"] by simp
 
 subsection\<open>Exposed faces\<close>
 
@@ -670,31 +655,31 @@
 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"
-by (force simp: exposed_face_of_def 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"
+  by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
 
 lemma exposed_face_of_Int_supporting_hyperplane_ge:
-   "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
-using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
+  "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
+  using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
 
 proposition exposed_face_of_Int:
   assumes "T exposed_face_of S"
-      and "u exposed_face_of S"
-    shows "(T \<inter> u) exposed_face_of S"
+      and "U exposed_face_of S"
+    shows "(T \<inter> U) exposed_face_of S"
 proof -
   obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
                and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
                and teq: "T = S \<inter> {x. a \<bullet> x = b}"
     using assms by (auto simp: exposed_face_of_def)
-  obtain a' b' where u: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
+  obtain a' b' where U: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
                  and s': "S \<subseteq> {x. a' \<bullet> x \<le> b'}"
-                 and ueq: "u = S \<inter> {x. a' \<bullet> x = b'}"
+                 and ueq: "U = S \<inter> {x. a' \<bullet> x = b'}"
     using assms by (auto simp: exposed_face_of_def)
-  have tu: "T \<inter> u face_of S"
-    using T teq u ueq by (simp add: face_of_Int)
+  have tu: "T \<inter> U face_of S"
+    using T teq U ueq by (simp add: face_of_Int)
   have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
     using S s' by (force simp: inner_left_distrib)
-  have "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'} \<and> T \<inter> u = S \<inter> {x. (a + a') \<bullet> x = b + b'}"
+  have "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'} \<and> T \<inter> U = S \<inter> {x. (a + a') \<bullet> x = b + b'}"
     using S s' by (fastforce simp: ss inner_left_distrib teq ueq)
   then show ?thesis
     using exposed_face_of_def tu by auto
@@ -860,8 +845,8 @@
   by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
 
 lemma face_of_singleton:
-   "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
-by (fastforce simp add: extreme_point_of_def face_of_def)
+  "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
+  by (fastforce simp add: extreme_point_of_def face_of_def)
 
 lemma extreme_point_not_in_REL_INTERIOR:
     fixes S :: "'a::real_normed_vector set"
@@ -871,11 +856,7 @@
 lemma extreme_point_not_in_interior:
   fixes S :: "'a::{real_normed_vector, perfect_space} set"
   assumes "x extreme_point_of S" shows "x \<notin> interior S"
-proof (cases "S = {x}")
-  case False
-  then show ?thesis
-    by (meson assms subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
-qed (simp add: empty_interior_finite)
+  using assms extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior by fastforce
 
 lemma extreme_point_of_face:
      "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
@@ -914,8 +895,8 @@
   by simp
 
 lemma extreme_point_of_Int:
-   "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
-by (simp add: extreme_point_of_def)
+  "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
+  by (simp add: extreme_point_of_def)
 
 lemma extreme_point_of_Int_supporting_hyperplane_le:
    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
@@ -965,16 +946,16 @@
   by (simp add: face_of_imp_subset facet_of_def)
 
 lemma hyperplane_facet_of_halfspace_le:
-   "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
-unfolding facet_of_def hyperplane_eq_empty
-by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
-           Suc_leI of_nat_diff aff_dim_halfspace_le)
+  "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
+  unfolding facet_of_def hyperplane_eq_empty
+  by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
+      Suc_leI of_nat_diff aff_dim_halfspace_le)
 
 lemma hyperplane_facet_of_halfspace_ge:
-    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
-unfolding facet_of_def hyperplane_eq_empty
-by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
-           Suc_leI of_nat_diff aff_dim_halfspace_ge)
+  "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
+  unfolding facet_of_def hyperplane_eq_empty
+  by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
+      Suc_leI of_nat_diff aff_dim_halfspace_ge)
 
 lemma facet_of_halfspace_le:
     "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
@@ -989,8 +970,8 @@
 qed
 
 lemma facet_of_halfspace_ge:
-    "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
-using facet_of_halfspace_le [of F "-a" "-b"] by simp
+  "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
+  using facet_of_halfspace_le [of F "-a" "-b"] by simp
 
 subsection \<open>Edges: faces of affine dimension 1\<close> (*FIXME too small subsection, rearrange? *)
 
@@ -1161,12 +1142,7 @@
     qed
 next
   show "convex hull {x. x extreme_point_of S} \<subseteq> S"
-  proof -
-    have "{a. a extreme_point_of S} \<subseteq> S"
-      using extreme_point_of_def by blast
-    then show ?thesis
-      by (simp add: \<open>convex S\<close> hull_minimal)
-  qed
+    using \<open>convex S\<close> extreme_point_of_stillconvex subset_hull by fastforce
 qed
 
 
@@ -1183,9 +1159,9 @@
 lemma extreme_points_of_convex_hull_eq:
   fixes S :: "'a::euclidean_space set"
   shows
-   "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
+    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
         \<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
-by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
+  by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
 
 
 lemma extreme_point_of_convex_hull_eq:
@@ -1221,33 +1197,23 @@
 lemma extreme_point_of_convex_hull_2:
   fixes x :: "'a::euclidean_space"
   shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
-proof -
-  have "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x \<in> {a,b}"
-    by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
-  then show ?thesis
-    by simp
-qed
+  by (simp add: extreme_point_of_convex_hull_affine_independent)
 
 lemma extreme_point_of_segment:
   fixes x :: "'a::euclidean_space"
-  shows
-   "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
-by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
+  shows "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
+  by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
 
 lemma face_of_convex_hull_subset:
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and T: "T face_of (convex hull S)"
-  obtains s' where "s' \<subseteq> S" "T = convex hull s'"
+  obtains S' where "S' \<subseteq> S" "T = convex hull S'"
 proof
   show "{x. x extreme_point_of T} \<subseteq> S"
     using T extreme_point_of_convex_hull extreme_point_of_face by blast
   show "T = convex hull {x. x extreme_point_of T}"
-  proof (rule Krein_Milman_Minkowski)
-    show "compact T"
-      using T assms compact_convex_hull face_of_imp_compact by auto
-    show "convex T"
-      using T face_of_imp_convex by blast
-  qed
+    by (metis Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull 
+        face_of_imp_compact face_of_imp_convex)
 qed
 
 
@@ -1431,14 +1397,14 @@
     by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
 next
   assume ?rhs
-  then obtain c where "c \<subseteq> S" and T: "T = convex hull c"
+  then obtain C where "C \<subseteq> S" and T: "T = convex hull C"
     by blast
-  have "affine hull c \<inter> affine hull (S - c) = {}"
-    by (intro disjoint_affine_hull [OF assms \<open>c \<subseteq> S\<close>], auto)
-  then have "affine hull c \<inter> convex hull (S - c) = {}"
+  have "affine hull C \<inter> affine hull (S - C) = {}"
+    by (intro disjoint_affine_hull [OF assms \<open>C \<subseteq> S\<close>], auto)
+  then have "affine hull C \<inter> convex hull (S - C) = {}"
     using convex_hull_subset_affine_hull by fastforce
   then show ?lhs
-    by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
+    by (metis face_of_convex_hulls \<open>C \<subseteq> S\<close> aff_independent_finite assms T)
 qed
 
 lemma facet_of_convex_hull_affine_independent:
@@ -1555,13 +1521,9 @@
 definition\<^marker>\<open>tag important\<close> polytope where
  "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
 
-lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
-proof -
-  have "\<And>a A. polytope A \<Longrightarrow> polytope ((+) a ` A)"
-    by (metis (no_types) convex_hull_translation finite_imageI polytope_def)
-  then show ?thesis
-    by (metis (no_types) add.left_inverse image_add_0 translation_assoc)
-qed
+lemma polytope_translation_eq: "polytope ((+) a ` S) \<longleftrightarrow> polytope S"
+  unfolding polytope_def
+  by (metis (no_types, opaque_lifting) add.left_inverse convex_hull_translation finite_imageI image_add_0 translation_assoc)
 
 lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
   unfolding polytope_def using convex_hull_linear_image by blast
@@ -1604,12 +1566,12 @@
 
 lemma polytope_scaling:
   assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
-by (simp add: assms polytope_linear_image)
+  by (simp add: assms polytope_linear_image)
 
 lemma polytope_imp_compact:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> compact S"
-by (metis finite_imp_compact_convex_hull polytope_def)
+  by (metis finite_imp_compact_convex_hull polytope_def)
 
 lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
   by (metis convex_convex_hull polytope_def)
@@ -1617,12 +1579,12 @@
 lemma polytope_imp_closed:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> closed S"
-by (simp add: compact_imp_closed polytope_imp_compact)
+  by (simp add: compact_imp_closed polytope_imp_compact)
 
 lemma polytope_imp_bounded:
   fixes S :: "'a::real_normed_vector set"
   shows "polytope S \<Longrightarrow> bounded S"
-by (simp add: compact_imp_bounded polytope_imp_compact)
+  by (simp add: compact_imp_bounded polytope_imp_compact)
 
 lemma polytope_interval: "polytope(cbox a b)"
   unfolding polytope_def by (meson closed_interval_as_convex_hull)