# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1587331017 -3600
# Node ID 7c0de1eb6075cd2ecf270134886bb2cea776a120
# Parent  33e886e21ed45b46c64ba101de6161f869b1f5dd
removal of symmetries in Polytope, plus some tidying

diff -r 33e886e21ed4 -r 7c0de1eb6075 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sun Apr 19 13:01:40 2020 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Sun Apr 19 22:16:57 2020 +0100
@@ -4,6 +4,7 @@
 
 theory Further_Topology
   imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts
+Sketch_and_Explore
 begin
 
 subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
@@ -28,10 +29,10 @@
     by (rule diff_f' derivative_intros differentiable_on_compose [where f=f] | force)+
   have geq: "g ` (S - {0}) = T - {0}"
   proof
-    have "g ` (S - {0}) \<subseteq> T"
-      apply (auto simp: g_def subspace_mul [OF \<open>subspace T\<close>])
-      apply (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
-      done
+    have "\<And>u. \<lbrakk>u \<in> S; norm u *\<^sub>R f (u /\<^sub>R norm u) \<notin> T\<rbrakk> \<Longrightarrow> u = 0"
+      by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
+    then have "g ` (S - {0}) \<subseteq> T"
+      using g_def by blast
     moreover have "g ` (S - {0}) \<subseteq> UNIV - {0}"
     proof (clarsimp simp: g_def)
       fix y
@@ -51,12 +52,14 @@
     proof -
       have "x /\<^sub>R norm x \<in> T"
         using \<open>subspace T\<close> subspace_mul that by blast
-      then show ?thesis
-        using * [THEN subsetD, of "x /\<^sub>R norm x"] that apply clarsimp
-        apply (rule_tac x="norm x *\<^sub>R xa" in image_eqI, simp)
-        apply (metis norm_eq_zero right_inverse scaleR_one scaleR_scaleR)
-        using \<open>subspace S\<close> subspace_mul apply force
-        done
+      then obtain u where u: "f u \<in> T" "x /\<^sub>R norm x = f u" "norm u = 1" "u \<in> S"
+        using * [THEN subsetD, of "x /\<^sub>R norm x"] \<open>x \<noteq> 0\<close> by auto
+      with that have [simp]: "norm x *\<^sub>R f u = x"
+        by (metis divideR_right norm_eq_zero)
+      moreover have "norm x *\<^sub>R u \<in> S - {0}"
+        using \<open>subspace S\<close> subspace_scale that(2) u by auto
+      with u show ?thesis
+        by (simp add: image_eqI [where x="norm x *\<^sub>R u"])
     qed
     then have "T - {0} \<subseteq> (\<lambda>x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S - {0})"
       by force
@@ -107,12 +110,10 @@
   qed (auto simp: p1span p2 span_base span_add)
   ultimately have "linear p1" "linear p2"
     by unfold_locales auto
-  have "(\<lambda>z. g (p1 z)) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
-    apply (rule differentiable_on_compose [where f=g])
-    apply (rule linear_imp_differentiable_on [OF \<open>linear p1\<close>])
-    apply (rule differentiable_on_subset [OF gdiff])
-    using p12_eq \<open>S \<subseteq> T\<close> apply auto
-    done
+  have "g differentiable_on p1 ` {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
+    using p12_eq \<open>S \<subseteq> T\<close>  by (force intro: differentiable_on_subset [OF gdiff])
+  then have "(\<lambda>z. g (p1 z)) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
+    by (rule differentiable_on_compose [OF linear_imp_differentiable_on [OF \<open>linear p1\<close>]])
   then have diff: "(\<lambda>x. g (p1 x) + p2 x) differentiable_on {x + y |x y. x \<in> S - {0} \<and> y \<in> T'}"
     by (intro derivative_intros linear_imp_differentiable_on [OF \<open>linear p2\<close>])
   have "dim {x + y |x y. x \<in> S - {0} \<and> y \<in> T'} \<le> dim {x + y |x y. x \<in> S  \<and> y \<in> T'}"
@@ -141,10 +142,7 @@
   proof clarsimp
     fix z assume "z \<notin> T'"
     show "\<exists>x y. z = x + y \<and> x \<in> g ` (S - {0}) \<and> y \<in> T'"
-      apply (rule_tac x="p1 z" in exI)
-      apply (rule_tac x="p2 z" in exI)
-      apply (simp add: p1 eq p2 geq)
-      by (metis \<open>z \<notin> T'\<close> add.left_neutral eq p2)
+      by (metis Diff_iff \<open>z \<notin> T'\<close> add.left_neutral eq geq p1 p2 singletonD)
   qed
   ultimately have "negligible (-T')"
     using negligible_subset by blast
@@ -173,8 +171,7 @@
   then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 \<inter> S) \<subseteq> T"
                 and g12: "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> norm(f x - g x) < 1/2"
     apply (rule Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"])
-    using fim apply auto
-    done
+    using fim by auto
   have gnz: "g x \<noteq> 0" if "x \<in> sphere 0 1 \<inter> S" for x
   proof -
     have "norm (f x) = 1"
@@ -190,10 +187,8 @@
     using gnz [of x]
     by (auto simp: subspace_mul [OF \<open>subspace T\<close>] subsetD [OF gim])
   have diffh: "h differentiable_on sphere 0 1 \<inter> S"
-    unfolding h_def
-    apply (intro derivative_intros diffg differentiable_on_compose [OF diffg])
-    using gnz apply auto
-    done
+    unfolding h_def using gnz
+    by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg])
   have homfg: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
   proof (rule homotopic_with_linear [OF contf])
     show "continuous_on (sphere 0 1 \<inter> S) g"
@@ -204,18 +199,19 @@
       have "f x \<in> sphere 0 1"
         using fim that by (simp add: image_subset_iff)
       moreover have "norm(f x - g x) < 1/2"
-        apply (rule g12)
-        using that by force
+        using g12 that by auto
       ultimately show ?thesis
         by (auto simp: norm_minus_commute dest: segment_bound)
     qed
-    show "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> T - {0}"
-      apply (simp add: subset_Diff_insert non0fg)
-      apply (simp add: segment_convex_hull)
-      apply (rule hull_minimal)
-       using fim image_eqI gim apply force
-      apply (rule subspace_imp_convex [OF \<open>subspace T\<close>])
-      done
+    show "closed_segment (f x) (g x) \<subseteq> T - {0}" if "x \<in> sphere 0 1 \<inter> S" for x
+    proof -
+      have "convex T"
+        by (simp add: \<open>subspace T\<close> subspace_imp_convex)
+      then have "convex hull {f x, g x} \<subseteq> T"
+        by (metis IntD2 closed_segment_subset fim gim image_subset_iff segment_convex_hull that)
+      then show ?thesis
+        using that non0fg segment_convex_hull by fastforce
+    qed
   qed
   obtain d where d: "d \<in> (sphere 0 1 \<inter> T) - h ` (sphere 0 1 \<inter> S)"
     using h spheremap_lemma1 [OF ST \<open>S \<subseteq> T\<close> diffh] by force
@@ -225,13 +221,17 @@
   have conth: "continuous_on (sphere 0 1 \<inter> S) h"
     using differentiable_imp_continuous_on diffh by blast
   have hom_hd: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
-    apply (rule homotopic_with_linear [OF conth continuous_on_const])
-    apply (simp add: subset_Diff_insert non0hd)
-    apply (simp add: segment_convex_hull)
-    apply (rule hull_minimal)
-     using h d apply (force simp: subspace_neg [OF \<open>subspace T\<close>])
-    apply (rule subspace_imp_convex [OF \<open>subspace T\<close>])
-    done
+  proof (rule homotopic_with_linear [OF conth continuous_on_const])
+    fix x
+    assume x: "x \<in> sphere 0 1 \<inter> S"
+    have "convex hull {h x, - d} \<subseteq> T"
+    proof (rule hull_minimal)
+      show "{h x, - d} \<subseteq> T"
+        using h d x by (force simp: subspace_neg [OF \<open>subspace T\<close>])
+    qed (simp add: subspace_imp_convex [OF \<open>subspace T\<close>])
+    with x segment_convex_hull show "closed_segment (h x) (- d) \<subseteq> T - {0}"
+      by (auto simp add: subset_Diff_insert non0hd)
+  qed
   have conT0: "continuous_on (T - {0}) (\<lambda>y. inverse(norm y) *\<^sub>R y)"
     by (intro continuous_intros) auto
   have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
@@ -242,13 +242,11 @@
        apply (rule homotopic_with_compose_continuous_left [OF hom_hd conT0 sub0T])
     using d apply (auto simp: h_def)
     done
-  show ?thesis
-    apply (rule_tac x=c in exI)
-    apply (rule homotopic_with_trans [OF _ homhc])
-    apply (rule homotopic_with_eq)
-       apply (rule homotopic_with_compose_continuous_left [OF homfg conT0 sub0T])
-      apply (auto simp: h_def)
-    done
+  have "homotopic_with_canon (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f h"
+    apply (rule homotopic_with_eq [OF homotopic_with_compose_continuous_left [OF homfg conT0 sub0T]])
+    by (auto simp: h_def)
+  then show ?thesis
+    by (metis homotopic_with_trans [OF _ homhc])
 qed
 
 
@@ -283,15 +281,21 @@
       then have affS_eq: "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
         using \<open>aff_dim T = aff_dim S\<close> by simp
       have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \<inter> T)"
-        apply (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
-          apply (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
-         apply (simp add: bounded_Int)
-        apply (rule affS_eq)
-        done
+      proof (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
+        show "convex (ball 0 1 \<inter> T)"
+          by (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
+        show "bounded (ball 0 1 \<inter> T)"
+          by (simp add: bounded_Int)
+        show "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
+          by (rule affS_eq)
+      qed
       also have "... = frontier (ball 0 1) \<inter> T"
-        apply (rule convex_affine_rel_frontier_Int [OF convex_ball])
-         apply (simp add: \<open>subspace T\<close> subspace_imp_affine)
-        using \<open>subspace T\<close> subspace_0 by force
+      proof (rule convex_affine_rel_frontier_Int [OF convex_ball])
+        show "affine T"
+          by (simp add: \<open>subspace T\<close> subspace_imp_affine)
+        show "interior (ball 0 1) \<inter> T \<noteq> {}"
+          using \<open>subspace T\<close> subspace_0 by force
+      qed
       also have "... = sphere 0 1 \<inter> T"
         by auto
       finally show ?thesis .
@@ -367,11 +371,10 @@
   next
     case False
     with \<open>\<not> s \<le> 0\<close> have "r > 0" "s > 0" by auto
-    show ?thesis
+    show thesis
       apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f])
-      using  \<open>0 < r\<close> \<open>0 < s\<close> assms(1)
-             apply (simp_all add: f aff_dim_cball)
-      using that by blast
+      using  \<open>0 < r\<close> \<open>0 < s\<close> assms(1) that
+      by (simp_all add: f aff_dim_cball inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f])
   qed
 qed
 
@@ -404,7 +407,6 @@
   show ?case
     apply (rule_tac x="\<lambda>x. if x \<in> S then f x else g x" in exI, simp)
     apply (intro conjI continuous_on_cases)
-    apply (simp_all add: insert closed_Union contf contg)
     using fim gim feq geq
     apply (force simp: insert closed_Union contf contg inf_commute intro: fg)+
     done
@@ -426,18 +428,18 @@
   assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
-      and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
+      and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S"
       and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
   obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
 proof (cases "\<F> - \<G> = {}")
   case True
-  then have "\<Union>\<F> \<subseteq> \<Union>\<G>"
-    by (simp add: Union_mono)
-  then show ?thesis
-    apply (rule_tac g=f in that)
-      using contf continuous_on_subset apply blast
-     using fim apply blast
-    by simp
+  show ?thesis
+  proof
+    show "continuous_on (\<Union> \<F>) f"
+      using True \<open>\<G> \<subseteq> \<F>\<close> contf by auto
+    show "f ` \<Union> \<F> \<subseteq> rel_frontier T"
+      using True fim by auto
+  qed auto
 next
   case False
   then have "0 \<le> aff_dim T"
@@ -446,19 +448,17 @@
     by (metis nonneg_eq_int)
   have Union_empty_eq: "\<Union>{D. D = {} \<and> P D} = {}" for P :: "'a set \<Rightarrow> bool"
     by auto
+  have face': "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
+    by (metis face inf_commute)
   have extendf: "\<exists>g. continuous_on (\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) g \<and>
                      g ` (\<Union> (\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) \<subseteq> rel_frontier T \<and>
                      (\<forall>x \<in> \<Union>\<G>. g x = f x)"
        if "i \<le> aff_dim T" for i::nat
   using that
   proof (induction i)
-    case 0 then show ?case
-      apply (simp add: Union_empty_eq)
-      apply (rule_tac x=f in exI)
-      apply (intro conjI)
-      using contf continuous_on_subset apply blast
-      using fim apply blast
-      by simp
+    case 0
+    show ?case
+      using 0 contf fim by (auto simp add: Union_empty_eq)
   next
     case (Suc p)
     with \<open>bounded T\<close> have "rel_frontier T \<noteq> {}"
@@ -477,12 +477,12 @@
       if D: "D \<in> \<G> \<union> ?Faces" for D
     proof (cases "D \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})")
       case True
-      then show ?thesis
-        apply (rule_tac x=h in exI)
-        apply (intro conjI)
-        apply (blast intro: continuous_on_subset [OF conth])
-        using him apply blast
-        by simp
+      have "continuous_on D h"
+        using True conth continuous_on_subset by blast
+      moreover have "h ` D \<subseteq> rel_frontier T"
+        using True him by blast
+      ultimately show ?thesis
+        by blast
     next
       case False
       note notDsub = False
@@ -507,9 +507,7 @@
         then have [simp]: "\<not> affine D"
           using affine_bounded_eq_trivial False \<open>D \<noteq> {}\<close> \<open>bounded D\<close> by blast
         have "{F. F facet_of D} \<subseteq> {E. E face_of C \<and> aff_dim E < int p}"
-          apply clarify
-          apply (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
-          done
+          by clarify (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq)
         moreover have "polyhedron D"
           using \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face_of_polytope_polytope poly polytope_imp_polyhedron by auto
         ultimately have relf_sub: "rel_frontier D \<subseteq> \<Union> {E. E face_of C \<and> aff_dim E < p}"
@@ -540,30 +538,39 @@
              if "E \<in> \<G> \<union> {D. Bex \<F> ((face_of) D) \<and> aff_dim D < int p}" for E
         proof (rule face_of_subset_rel_frontier)
           show "D \<inter> E face_of D"
-            using that \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face
-            apply auto
-            apply (meson face_of_Int_subface \<open>\<G> \<subseteq> \<F>\<close> face_of_refl_eq poly polytope_imp_convex subsetD)
-            using face_of_Int_subface apply blast
-            done
+            using that
+          proof safe
+            assume "E \<in> \<G>"
+            then show "D \<inter> E face_of D"
+              by (meson \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> assms(2) face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex subsetD)
+          next
+            fix x
+            assume "aff_dim E < int p" "x \<in> \<F>" "E face_of x"
+            then show "D \<inter> E face_of D"
+              by (meson \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face' face_of_Int_subface that)
+          qed
           show "D \<inter> E \<noteq> D"
             using that notDsub by auto
         qed
-        then show ?thesis
-          apply (rule_tac x=g in exI)
-          apply (intro conjI ballI)
-            using continuous_on_subset contg apply blast
-           using gim apply blast
-          using gh by fastforce
+        moreover have "continuous_on D g"
+          using contg continuous_on_subset by blast
+        ultimately show ?thesis
+          by (rule_tac x=g in exI) (use gh gim in fastforce)
       qed
     qed
     have intle: "i < 1 + int j \<longleftrightarrow> i \<le> int j" for i j
       by auto
     have "finite \<G>"
       using \<open>finite \<F>\<close> \<open>\<G> \<subseteq> \<F>\<close> rev_finite_subset by blast
-    then have fin: "finite (\<G> \<union> ?Faces)"
-      apply simp
-      apply (rule_tac B = "\<Union>{{D. D face_of C}| C. C \<in> \<F>}" in finite_subset)
-       by (auto simp: \<open>finite \<F>\<close> finite_polytope_faces poly)
+    moreover have "finite (?Faces)"
+    proof -
+      have \<section>: "finite (\<Union> {{D. D face_of C} |C. C \<in> \<F>})"
+        by (auto simp: \<open>finite \<F>\<close> finite_polytope_faces poly)
+      show ?thesis
+        by (auto intro: finite_subset [OF _ \<section>])
+    qed
+    ultimately have fin: "finite (\<G> \<union> ?Faces)"
+      by simp
     have clo: "closed S" if "S \<in> \<G> \<union> ?Faces" for S
       using that \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly polytope_imp_closed by blast
     have K: "X \<inter> Y \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int p})"
@@ -571,9 +578,7 @@
     proof -
       have ff: "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
         if XY: "X face_of D" "Y face_of E" and DE: "D \<in> \<F>" "E \<in> \<F>" for D E
-        apply (rule face_of_Int_subface [OF _ _ XY])
-        apply (auto simp: face DE)
-        done
+        by (rule face_of_Int_subface [OF _ _ XY]) (auto simp: face' DE)
       show ?thesis
         using that
         apply auto
@@ -586,22 +591,19 @@
                    "g ` \<Union>(\<G> \<union> ?Faces) \<subseteq> rel_frontier T"
                    "(\<forall>x \<in> \<Union>(\<G> \<union> ?Faces) \<inter>
                           \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < p}). g x = h x)"
-      apply (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+)
-      done
+      by (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+)
     then show ?case
-      apply (simp add: intle local.heq [symmetric], blast)
-      done
+      by (simp add: intle local.heq [symmetric], blast)
   qed
   have eq: "\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i}) = \<Union>\<F>"
   proof
     show "\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}) \<subseteq> \<Union>\<F>"
-      apply (rule Union_subsetI)
-      using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset  apply force
-      done
+      using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset by fastforce
     show "\<Union>\<F> \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < i})"
-      apply (rule Union_mono)
-      using face  apply (fastforce simp: aff i)
-      done
+    proof (rule Union_mono)
+      show "\<F> \<subseteq> \<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}"
+        using face by (fastforce simp: aff i)
+    qed
   qed
   have "int i \<le> aff_dim T" by (simp add: i)
   then show ?thesis
@@ -647,13 +649,15 @@
       by (simp add: C card_insert_if insert.hyps le_SucI)
     have "closed (\<Union>\<F>)"
       using clo insert.hyps by blast
+    have "continuous_on (X - insert a C) f"
+      using contf by (force simp: elim: continuous_on_subset)
+    moreover have "continuous_on (\<Union> \<F> - insert a C) g"
+      using contg by (force simp: elim: continuous_on_subset)
+    ultimately
     have "continuous_on (X - insert a C \<union> (\<Union>\<F> - insert a C)) (\<lambda>x. if x \<in> X then f x else g x)"
-       apply (rule continuous_on_cases_local)
-          apply (simp_all add: closedin_closed)
+      apply (intro continuous_on_cases_local; simp add: closedin_closed)
         using \<open>closed X\<close> apply blast
         using \<open>closed (\<Union>\<F>)\<close> apply blast
-        using contf apply (force simp: elim: continuous_on_subset)
-        using contg apply (force simp: elim: continuous_on_subset)
         using fh gh insert.hyps pwX by fastforce
     then show "continuous_on (\<Union>(insert X \<F>) - insert a C) (\<lambda>a. if a \<in> X then f a else g a)"
       by (blast intro: continuous_on_subset)
@@ -687,9 +691,7 @@
   obtain C g where "finite C \<and> disjnt C U \<and> card C \<le> card ?\<F> \<and>
                  continuous_on (\<Union>?\<F> - C) g \<and> g ` (\<Union>?\<F> - C) \<subseteq> T
                   \<and> (\<forall>x \<in> (\<Union>?\<F> - C) \<inter> K. g x = h x)"
-    apply (rule exE [OF extend_map_lemma_cofinite0 [OF fin pw, of U T h]])
-      apply (fastforce intro!:  clo \<F>)+
-    done
+    using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo \<F>)
   ultimately show ?thesis
     by (rule_tac C=C and g=g in that) auto
 qed
@@ -699,7 +701,7 @@
   assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
-      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T"
   obtains C g where
      "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
@@ -708,28 +710,23 @@
   define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
   have "finite \<G>"
     using assms finite_subset by blast
-  moreover have "finite (\<Union>{{D. D face_of C} |C. C \<in> \<F>})"
-    apply (rule finite_Union)
-     apply (simp add: \<open>finite \<F>\<close>)
-    using finite_polytope_faces poly by auto
-  ultimately have "finite \<H>"
-    apply (simp add: \<H>_def)
-    apply (rule finite_subset [of _ "\<Union> {{D. D face_of C} | C. C \<in> \<F>}"], auto)
-    done
-  have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+  have *: "finite (\<Union>{{D. D face_of C} |C. C \<in> \<F>})"
+    using finite_polytope_faces poly \<open>finite \<F>\<close> by force
+  then have "finite \<H>"
+    by (auto simp: \<H>_def \<open>finite \<G>\<close> intro: finite_subset [OF _ *])
+  have face': "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
+    by (metis face inf_commute)
+  have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
     unfolding \<H>_def
-    apply (elim UnE bexE CollectE DiffE)
-    using subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] apply (simp_all add: face)
-      apply (meson subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] face face_of_Int_subface face_of_imp_subset face_of_refl poly polytope_imp_convex)+
+    using subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] apply (auto simp add: face)
+    apply (meson face' face_of_Int_subface face_of_refl_eq poly polytope_imp_convex)+
     done
   obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h ` (\<Union>\<H>) \<subseteq> rel_frontier T"
-             and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x"
-    using \<open>finite \<H>\<close>
-    unfolding \<H>_def
-    apply (rule extend_map_lemma [OF _ Un_upper1 T _ _ _ contf fim])
-    using \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly apply fastforce
-    using * apply (auto simp: \<H>_def)
-    done
+             and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x" 
+  proof (rule extend_map_lemma [OF \<open>finite \<H>\<close> [unfolded \<H>_def] Un_upper1 T])
+    show "\<And>X. \<lbrakk>X \<in> \<G> \<union> {D. \<exists>C\<in>\<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}\<rbrakk> \<Longrightarrow> polytope X"
+      using \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly by fastforce
+  qed (use * \<H>_def contf fim in auto)
   have "bounded (\<Union>\<G>)"
     using \<open>finite \<G>\<close> \<open>\<G> \<subseteq> \<F>\<close> poly polytope_imp_bounded by blast
   then have "\<Union>\<G> \<noteq> UNIV"
@@ -783,7 +780,7 @@
             fix E
             assume "b \<in> E" "E \<in> \<G>"
             then have "E \<inter> D face_of E \<and> E \<inter> D face_of D"
-              using \<open>\<G> \<subseteq> \<F>\<close> face that by auto
+              using \<open>\<G> \<subseteq> \<F>\<close> face' that by auto
             with face_of_subset_rel_frontier \<open>E \<in> \<G>\<close> \<open>b \<in> E\<close> brelD rel_interior_subset [of D]
                  D_not_subset rel_frontier_def \<H>_def
             show False
@@ -824,11 +821,10 @@
             next
               case 2 show ?thesis
               proof (rule face_of_subset_rel_frontier [THEN subsetD])
-                show "D \<inter> A face_of D"
-                  apply (rule face_of_Int_subface [of D B _ A, THEN conjunct1])
-                     apply (simp_all add: 2 \<open>D \<in> \<F>\<close> face)
-                   apply (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex face_of_refl)
-                  done
+                have "D face_of D"
+                  by (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex face_of_refl)
+                then show "D \<inter> A face_of D"
+                  by (meson "2"(2) "2"(3) \<open>D \<in> \<F>\<close> face' face_of_Int_Int face_of_face)
                 show "D \<inter> A \<noteq> D"
                   using "2" D_not_subset \<H>_def by blast
               qed (auto simp: 2)
@@ -873,7 +869,7 @@
   assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T"
-      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
   obtains g where "continuous_on (\<Union>\<F>) g"
      "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
@@ -888,7 +884,7 @@
              and diaG: "\<And>X. X \<in> \<G> \<Longrightarrow> diameter X < d"
              and polyG: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
              and affG: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T - 1"
-             and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+             and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
   proof (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly _ face])
     show "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T - 1"
       by (simp add: aff)
@@ -928,7 +924,7 @@
   assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T"
-      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
   obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
      "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
@@ -943,7 +939,7 @@
              and diaG: "\<And>X. X \<in> \<G> \<Longrightarrow> diameter X < d"
              and polyG: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
              and affG: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T"
-             and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+             and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
     by (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly aff face]) auto
   obtain C h where "finite C" and dis: "disjnt C (\<Union>(\<G> \<inter> Pow V))"
                and card: "card C \<le> card \<G>" and conth: "continuous_on (\<Union>\<G> - C) h"
@@ -978,8 +974,7 @@
     show "h x = f x" if "x \<in> S" for x
     proof -
       have "h x = g x"
-        apply (rule hg)
-        using Ssub that by blast
+        using Ssub hg that by blast
       also have "... = f x"
         by (simp add: gf that)
       finally show "h x = f x" .
@@ -1054,7 +1049,7 @@
         using \<open>compact S\<close> compact_eq_bounded_closed by auto
       show poly: "\<And>X. X \<in> {bbox \<inter> T} \<Longrightarrow> polytope X"
         by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron \<open>affine T\<close>)
-      show "\<And>X Y. \<lbrakk>X \<in> {bbox \<inter> T}; Y \<in> {bbox \<inter> T}\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+      show "\<And>X Y. \<lbrakk>X \<in> {bbox \<inter> T}; Y \<in> {bbox \<inter> T}\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
         by (simp add:poly face_of_refl polytope_imp_convex)
       show "\<And>X. X \<in> {bbox \<inter> T} \<Longrightarrow> aff_dim X \<le> aff_dim U"
         by (simp add: \<open>aff_dim (bbox \<inter> T) \<le> aff_dim U\<close>)
@@ -3886,7 +3881,7 @@
       by (auto simp: homotopic_with_imp_continuous dest: homotopic_with_imp_subset1 homotopic_with_imp_subset2)
   next
     assume ?rhs then show ?lhs
-      by (force simp: elim: homotopic_with_eq dest: homotopic_with_sphere_times [where h=g])
+      by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force)
   qed
   then show ?thesis
     by (simp add: *)
diff -r 33e886e21ed4 -r 7c0de1eb6075 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sun Apr 19 13:01:40 2020 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Sun Apr 19 22:16:57 2020 +0100
@@ -2913,7 +2913,7 @@
   assumes "finite \<F>"
       and "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
-      and "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
+      and "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
       and "finite I"
     shows "\<exists>\<G>. \<Union>\<G> = \<Union>\<F> \<and>
                  finite \<G> \<and>
@@ -2921,7 +2921,7 @@
                  (\<forall>C \<in> \<F>. \<forall>x \<in> C. \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C) \<and>
                  (\<forall>X \<in> \<G>. polytope X) \<and>
                  (\<forall>X \<in> \<G>. aff_dim X \<le> d) \<and>
-                 (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
+                 (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X) \<and>
                  (\<forall>X \<in> \<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
                           (a,b) \<in> I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
                                         a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b)"
@@ -2937,7 +2937,7 @@
                    and sub2: "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C"
                    and poly: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
                    and aff: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> d"
-                   and face: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+                   and face: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
                    and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<G>; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
                                     a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
     by (auto simp: that)
@@ -2960,7 +2960,7 @@
                           (a,b) \<in> insert ab I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
                                                   a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
       using \<open>ab = (a, b)\<close> I by fastforce
-    show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+    show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X"
       by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge)
     show "\<forall>C \<in> ?\<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
       using sub1 by force
@@ -2984,10 +2984,10 @@
   assumes "0 < e" "finite \<F>"
       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
-      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+      and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
   obtains "\<F>'" where "finite \<F>'" "\<Union>\<F>' = \<Union>\<F>" "\<And>X. X \<in> \<F>' \<Longrightarrow> diameter X < e"
                 "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X" "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
-                "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+                "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
                 "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
                 "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<F>' \<and> x \<in> D \<and> D \<subseteq> C"
 proof -
@@ -3009,7 +3009,7 @@
   obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
               and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
               and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
-              and face: "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+              and face: "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
               and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
                                      a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
               and sub1: "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
@@ -3214,15 +3214,13 @@
         finite \<C> \<and>
         (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
         (\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
-        (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
-                \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
+        (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C> \<longrightarrow> (S \<inter> S') face_of S)"
 
 definition\<^marker>\<open>tag important\<close> triangulation where
  "triangulation \<T> \<equiv>
         finite \<T> \<and>
         (\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
-        (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T>
-                \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
+        (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T> \<longrightarrow> (T \<inter> T') face_of T)"
 
 
 subsection\<open>Refining a cell complex to a simplicial complex\<close>
@@ -3312,7 +3310,7 @@
       and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
       and "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
-      and "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      and "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
     shows "\<exists>\<T>. simplicial_complex \<T> \<and>
                 (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
                 \<Union>\<T> = \<Union>\<M> \<and>
@@ -3322,9 +3320,9 @@
 proof (induction n arbitrary: \<M> rule: less_induct)
   case (less n)
   then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
-      and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
-      and face\<M>:   "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
-      and intface\<M>: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+    and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
+    and face\<M>:   "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
+    and intface\<M>: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
     by metis+
   show ?case
   proof (cases "n \<le> 1")
@@ -3339,22 +3337,22 @@
     case False
     define \<S> where "\<S> \<equiv> {C \<in> \<M>. aff_dim C < n}"
     have "finite \<S>" "\<And>C. C \<in> \<S> \<Longrightarrow> polytope C" "\<And>C. C \<in> \<S> \<Longrightarrow> aff_dim C \<le> int (n - 1)"
-         "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
-         "\<And>C1 C2. \<lbrakk>C1 \<in> \<S>; C2 \<in> \<S>\<rbrakk>  \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
+      "\<And>C1 C2. \<lbrakk>C1 \<in> \<S>; C2 \<in> \<S>\<rbrakk>  \<Longrightarrow> C1 \<inter> C2 face_of C1"
       using less.prems
-      apply (auto simp: \<S>_def)
+          apply (auto simp: \<S>_def)
       by (metis aff_dim_subset face_of_imp_subset less_le not_le)
     with less.IH [of "n-1" \<S>] False
     obtain \<U> where "simplicial_complex \<U>"
-           and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
-           and        "\<Union>\<U> = \<Union>\<S>"
-           and fin\<U>:  "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
-           and C\<U>:    "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
+      and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
+      and        "\<Union>\<U> = \<Union>\<S>"
+      and fin\<U>:  "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
+      and C\<U>:    "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
       by auto
     then have "finite \<U>"
-         and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
-         and face\<U>:  "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
-         and faceI\<U>: "\<And>S S'. \<lbrakk>S \<in> \<U>; S' \<in> \<U>\<rbrakk> \<Longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S'"
+      and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
+      and face\<U>:  "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
+      and faceI\<U>: "\<And>S S'. \<lbrakk>S \<in> \<U>; S' \<in> \<U>\<rbrakk> \<Longrightarrow> (S \<inter> S') face_of S"
       by (auto simp: simplicial_complex_def)
     define \<N> where "\<N> \<equiv> {C \<in> \<M>. aff_dim C = n}"
     have "finite \<N>"
@@ -3364,7 +3362,7 @@
       and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
       by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
     have in_rel_interior: "(SOME z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
-        using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
+      using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
     have *: "\<exists>T. \<not> affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
       if "K \<in> \<U>" for K
     proof -
@@ -3392,7 +3390,7 @@
           by (simp add: \<open>closed C\<close> rel_frontier_def subset_iff)
         finally have "K \<subseteq> C" .
         have "L \<inter> C face_of C"
-          using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by auto
+          using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by (simp add: inf_commute)
         moreover have "L \<inter> C \<noteq> C"
           using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close>
           apply (clarsimp simp: \<N>_def \<S>_def)
@@ -3480,192 +3478,185 @@
           ultimately show ?thesis
             using that by auto
         qed
-        have "(S \<inter> S' face_of S) \<and> (S \<inter> S' face_of S')"
-          if "S \<in> \<U> \<union> ?\<T>" "S' \<in> \<U> \<union> ?\<T>" for S S'
+        have \<section>: "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+          if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
         proof -
-          have symmy: "\<lbrakk>\<And>X Y. R X Y \<Longrightarrow> R Y X;
-                        \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> \<U>\<rbrakk> \<Longrightarrow> R X Y;
-                        \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y;
-                        \<And>X Y. \<lbrakk>X \<in> ?\<T>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y\<rbrakk> \<Longrightarrow> R S S'" for R
-            using that by (metis (no_types, lifting) Un_iff)
-          show ?thesis
-          proof (rule symmy)
-            show "Y \<inter> X face_of Y \<and> Y \<inter> X face_of X"
-              if "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" for X Y :: "'a set"
-              by (simp add: inf_commute that)
-          next
-            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
-              if "X \<in> \<U>" and "Y \<in> \<U>" for X Y
-              by (simp add: faceI\<U> that)
-          next
-            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
-              if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
-            proof -
-              obtain C K
-                where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
-                and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
-                using XY by blast
-              have "convex C"
-                by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
-              have "K \<subseteq> C"
-                by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
-              let ?z = "(SOME z. z \<in> rel_interior C)"
-              have z: "?z \<in> rel_interior C"
-                using \<open>C \<in> \<N>\<close> in_rel_interior by blast
-              obtain D where "D \<in> \<S>" "X \<subseteq> D"
-                using C\<U> \<open>X \<in> \<U>\<close> by blast
-              have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
-                using rel_interior_subset by blast
-              also have "(C \<inter> D) \<inter> rel_interior C = {}"
-              proof (rule face_of_disjoint_rel_interior)
-                show "C \<inter> D face_of C"
-                  using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
-                show "C \<inter> D \<noteq> C"
-                  by (metis (mono_tags, lifting) Int_lower2 \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> aff_dim_subset mem_Collect_eq not_le)
-              qed
-              finally have DC: "D \<inter> rel_interior C = {}" .
-              have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
-                apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
-                using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
-              obtain I where I: "\<not> affine_dependent I"
-                         and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
-                using "*" \<open>K \<in> \<U>\<close> by force
-              then have "?z \<notin> affine hull I"
-                using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull z by blast
-              have "X \<inter> K face_of K"
-                by (simp add: \<open>K \<in> \<U>\<close> faceI\<U> \<open>X \<in> \<U>\<close>)
-              also have "... face_of convex hull insert ?z K"
-                by (metis I Keq \<open>?z \<notin> affine hull I\<close> aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert)
-              finally have "X \<inter> K face_of convex hull insert ?z K" .
-              then show ?thesis
-                using "*" \<open>K \<in> \<U>\<close> faceI\<U> that(1) by (fastforce simp add: Y eq)
-            qed
-          next
-            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
-              if XY: "X \<in> ?\<T>" "Y \<in> ?\<T>" for X Y
-            proof -
-              obtain C K D L
-                where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+          obtain C K
+            where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+              and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
+            using XY by blast
+          have "convex C"
+            by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+          have "K \<subseteq> C"
+            by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
+          let ?z = "(SOME z. z \<in> rel_interior C)"
+          have z: "?z \<in> rel_interior C"
+            using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+          obtain D where "D \<in> \<S>" "X \<subseteq> D"
+            using C\<U> \<open>X \<in> \<U>\<close> by blast
+          have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
+            using rel_interior_subset by blast
+          also have "(C \<inter> D) \<inter> rel_interior C = {}"
+          proof (rule face_of_disjoint_rel_interior)
+            show "C \<inter> D face_of C"
+              using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
+            show "C \<inter> D \<noteq> C"
+              by (metis (mono_tags, lifting) Int_lower2 \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> aff_dim_subset mem_Collect_eq not_le)
+          qed
+          finally have DC: "D \<inter> rel_interior C = {}" .
+          have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
+            apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
+            using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
+          obtain I where I: "\<not> affine_dependent I"
+            and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
+            using "*" \<open>K \<in> \<U>\<close> by force
+          then have "?z \<notin> affine hull I"
+            using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull z by blast
+          have "X \<inter> K face_of K"
+            by (simp add: XY(1) \<open>K \<in> \<U>\<close> faceI\<U> inf_commute)
+          also have "... face_of convex hull insert ?z K"
+            by (metis I Keq \<open>?z \<notin> affine hull I\<close> aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert)
+          finally have "X \<inter> K face_of convex hull insert ?z K" .
+          then show ?thesis
+            by (simp add: XY(1) Y \<open>K \<in> \<U>\<close> eq faceI\<U>)
+        qed
+
+        show "S \<inter> S' face_of S"
+          if "S \<in> \<U> \<union> ?\<T> \<and> S' \<in> \<U> \<union> ?\<T>" for S S'
+          using that
+        proof (elim conjE UnE)
+          fix X Y
+          assume "X \<in> \<U>" and "Y \<in> \<U>"
+          then show "X \<inter> Y face_of X"
+            by (simp add: faceI\<U>)
+        next
+          fix X Y
+          assume XY: "X \<in> \<U>" "Y \<in> ?\<T>"
+          then show "X \<inter> Y face_of X" "Y \<inter> X face_of Y"
+            using \<section> [OF XY] by (auto simp: Int_commute)
+        next
+          fix X Y
+          assume XY: "X \<in> ?\<T>" "Y \<in> ?\<T>"
+          show "X \<inter> Y face_of X"
+          proof -
+            obtain C K D L
+              where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
                 and X: "X = convex hull insert (SOME z. z \<in> rel_interior C) K"
                 and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
                 and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior D) L"
-                using XY by blast
-              let ?z = "(SOME z. z \<in> rel_interior C)"
-              have z: "?z \<in> rel_interior C"
-                using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+              using XY by blast
+            let ?z = "(SOME z. z \<in> rel_interior C)"
+            have z: "?z \<in> rel_interior C"
+              using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+            have "convex C"
+              by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+            have "convex K"
+              using "*" \<open>K \<in> \<U>\<close> by blast
+            have "convex L"
+              by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
+            show ?thesis
+            proof (cases "D=C")
+              case True
+              then have "L \<subseteq> rel_frontier C"
+                using \<open>L \<subseteq> rel_frontier D\<close> by auto
+              show ?thesis
+                apply (simp add: X Y True)
+                apply (simp add: convex_hull_insert_Int_eq [OF z] \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> \<open>convex C\<close> \<open>convex K\<close> \<open>convex L\<close>)
+                using face_of_polytope_insert2
+                by (metis "*" IntI \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close>\<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> aff_independent_finite ahK_C_disjoint empty_iff faceI\<U> polytope_convex_hull z)
+            next
+              case False
+              have "convex D"
+                by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
+              have "K \<subseteq> C"
+                by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
+              have "L \<subseteq> D"
+                by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
+              let ?w = "(SOME w. w \<in> rel_interior D)"
+              have w: "?w \<in> rel_interior D"
+                using \<open>D \<in> \<N>\<close> in_rel_interior by blast
+              have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
+                using rel_interior_subset by blast
+              also have "(D \<inter> C) \<inter> rel_interior D = {}"
+              proof (rule face_of_disjoint_rel_interior)
+                show "D \<inter> C face_of D"
+                  using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
+                have "D \<in> \<M> \<and> aff_dim D = int n"
+                  using \<N>_def \<open>D \<in> \<N>\<close> by blast
+                moreover have "C \<in> \<M> \<and> aff_dim C = int n"
+                  using \<N>_def \<open>C \<in> \<N>\<close> by blast
+                ultimately show "D \<inter> C \<noteq> D"
+                  by (metis Int_commute False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
+              qed
+              finally have CD: "C \<inter> (rel_interior D) = {}" .
+              have zKC: "(convex hull insert ?z K) \<subseteq> C"
+                by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed convex\<N> hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z)
+              have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
+                          convex hull (insert ?z K) \<inter> convex hull L"
+                apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
+                using zKC CD apply (force simp: disjnt_def)
+                done
+              have ch_id: "convex hull K = K" "convex hull L = L"
+                using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
               have "convex C"
                 by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
-              have "convex K"
-                using "*" \<open>K \<in> \<U>\<close> by blast
-              have "convex L"
-                by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
-              show ?thesis
-              proof (cases "D=C")
-                case True
-                then have "L \<subseteq> rel_frontier C"
-                  using \<open>L \<subseteq> rel_frontier D\<close> by auto
-                show ?thesis
-                  apply (simp add: X Y True)
-                  apply (simp add: convex_hull_insert_Int_eq [OF z] \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> \<open>convex C\<close> \<open>convex K\<close> \<open>convex L\<close>)
-                  using face_of_polytope_insert2
-                  by (metis "*" IntI \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close>\<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> aff_independent_finite ahK_C_disjoint empty_iff faceI\<U> polytope_convex_hull z)
-              next
-                case False
-                have "convex D"
-                  by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
-                have "K \<subseteq> C"
-                  by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
-                have "L \<subseteq> D"
-                  by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
-                let ?w = "(SOME w. w \<in> rel_interior D)"
-                have w: "?w \<in> rel_interior D"
-                  using \<open>D \<in> \<N>\<close> in_rel_interior by blast
-                have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
-                  using rel_interior_subset by blast
-                also have "(D \<inter> C) \<inter> rel_interior D = {}"
+              have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
+                by blast
+              also have "... = convex hull K \<inter> L"
+              proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
+                have "(C \<inter> D) \<inter> rel_interior C = {}"
                 proof (rule face_of_disjoint_rel_interior)
-                  show "D \<inter> C face_of D"
+                  show "C \<inter> D face_of C"
                     using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
-                  have "D \<in> \<M> \<and> aff_dim D = int n"
-                    using \<N>_def \<open>D \<in> \<N>\<close> by blast
-                  moreover have "C \<in> \<M> \<and> aff_dim C = int n"
-                    using \<N>_def \<open>C \<in> \<N>\<close> by blast
-                  ultimately show "D \<inter> C \<noteq> D"
-                    by (metis False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
+                  have "D \<in> \<M>" "aff_dim D = int n"
+                    using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
+                  moreover have "C \<in> \<M>" "aff_dim C = int n"
+                    using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
+                  ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
+                    by fastforce
+                  then have "\<not> C face_of D"
+                    using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
+                  show "C \<inter> D \<noteq> C"
+                    by (metis inf_commute \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M>)
                 qed
-                finally have CD: "C \<inter> (rel_interior D) = {}" .
-                have zKC: "(convex hull insert ?z K) \<subseteq> C"
-                  by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed convex\<N> hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z)
-                have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
-                          convex hull (insert ?z K) \<inter> convex hull L"
-                  apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
-                  using zKC CD apply (force simp: disjnt_def)
-                  done
-                have ch_id: "convex hull K = K" "convex hull L = L"
-                  using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
-                have "convex C"
-                  by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
-                have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
-                  by blast
-                also have "... = convex hull K \<inter> L"
-                proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
-                  have "(C \<inter> D) \<inter> rel_interior C = {}"
-                  proof (rule face_of_disjoint_rel_interior)
-                    show "C \<inter> D face_of C"
-                      using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
-                    have "D \<in> \<M>" "aff_dim D = int n"
-                      using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
-                    moreover have "C \<in> \<M>" "aff_dim C = int n"
-                      using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
-                    ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
-                      by fastforce
-                    then have "\<not> C face_of D"
-                      using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
-                    show "C \<inter> D \<noteq> C"
-                      using \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M> by fastforce
-                  qed
-                  then have "D \<inter> rel_interior C = {}"
-                    by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset)
-                  then show "disjnt L (rel_interior C)"
-                    by (meson \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
-                next
-                  show "L \<inter> convex hull K = convex hull K \<inter> L"
-                    by force
-                qed
-                finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
-                have "convex hull insert ?z K \<inter> convex hull L face_of K"
-                  by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
-                also have "... face_of convex hull insert ?z K"
-                proof -
-                  obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
-                    using * [OF \<open>K \<in> \<U>\<close>] by auto
-                  then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
-                    using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull by blast
-                  then show ?thesis
-                    by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
-                qed
-                finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
-                have "convex hull insert ?z K \<inter> convex hull L face_of L"
-                  by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
-                also have "... face_of convex hull insert ?w L"
-                proof -
-                  obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
-                    using * [OF \<open>L \<in> \<U>\<close>] by auto
-                  then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
-                    using \<open>D \<in> \<N>\<close> \<open>L \<in> \<U>\<close> \<open>L \<subseteq> rel_frontier D\<close> affine_hull_convex_hull ahK_C_disjoint by blast
-                  then show ?thesis
-                    by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
-                qed
-                finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
-                show ?thesis
-                  by (simp add: X Y eq 1 2)
+                then have "D \<inter> rel_interior C = {}"
+                  by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset)
+                then show "disjnt L (rel_interior C)"
+                  by (meson \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
+              next
+                show "L \<inter> convex hull K = convex hull K \<inter> L"
+                  by force
               qed
+              finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
+              have "convex hull insert ?z K \<inter> convex hull L face_of K"
+                by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
+              also have "... face_of convex hull insert ?z K"
+              proof -
+                obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
+                  using * [OF \<open>K \<in> \<U>\<close>] by auto
+                then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
+                  using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull by blast
+                then show ?thesis
+                  by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
+              qed
+              finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
+              have "convex hull insert ?z K \<inter> convex hull L face_of L"
+                by (metis \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> chKL ch_id faceI\<U> inf_commute)
+              also have "... face_of convex hull insert ?w L"
+              proof -
+                obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
+                  using * [OF \<open>L \<in> \<U>\<close>] by auto
+                then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
+                  using \<open>D \<in> \<N>\<close> \<open>L \<in> \<U>\<close> \<open>L \<subseteq> rel_frontier D\<close> affine_hull_convex_hull ahK_C_disjoint by blast
+                then show ?thesis
+                  by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
+              qed
+              finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
+              show ?thesis
+                by (simp add: X Y eq 1 2)
             qed
           qed
-        qed
-        then
-        show "S \<inter> S' face_of S" "S \<inter> S' face_of S'" if "S \<in> \<U> \<union> ?\<T> \<and> S' \<in> \<U> \<union> ?\<T>" for S S'
-          using that by auto
+        qed 
       qed
       show "\<exists>F \<subseteq> \<U> \<union> ?\<T>. C = \<Union>F" if "C \<in> \<M>" for C
       proof (cases "C \<in> \<S>")
@@ -3772,7 +3763,7 @@
 lemma simplicial_subdivision_of_cell_complex_lowdim:
   assumes "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
-      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
       and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> d"
   obtains \<T> where "simplicial_complex \<T>" "\<And>K. K \<in> \<T> \<Longrightarrow> aff_dim K \<le> d"
                   "\<Union>\<T> = \<Union>\<M>"
@@ -3800,10 +3791,13 @@
       if "G \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F face_of G" for F G
       using that face_of_trans by blast
   next
-    show "F1 \<inter> F2 face_of F1 \<and> F1 \<inter> F2 face_of F2"
-      if "F1 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F2 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F1 F2
-      using that
-      by safe (meson face face_of_Int_subface)+
+    fix F1 F2
+    assume "F1 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F2 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})"
+    then obtain C1 C2 where "C1 \<in> \<M>" "C2 \<in> \<M>" and F: "F1 face_of C1" "F2 face_of C2"
+      by auto
+    show "F1 \<inter> F2 face_of F1"
+      using face_of_Int_subface [OF _ _ F]
+      by (metis \<open>C1 \<in> \<M>\<close> \<open>C2 \<in> \<M>\<close> face inf_commute)
   qed
   moreover
   have "\<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) = \<Union>\<M>"
@@ -3838,7 +3832,7 @@
 proposition simplicial_subdivision_of_cell_complex:
   assumes "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
-      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
   obtains \<T> where "simplicial_complex \<T>"
                   "\<Union>\<T> = \<Union>\<M>"
                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
@@ -3848,7 +3842,7 @@
 corollary fine_simplicial_subdivision_of_cell_complex:
   assumes "0 < e" "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
-      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
   obtains \<T> where "simplicial_complex \<T>"
                   "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
                   "\<Union>\<T> = \<Union>\<M>"
@@ -3857,7 +3851,7 @@
 proof -
   obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>" 
               and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
-               and      "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+               and      "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
                and \<N>covers: "\<And>C x. C \<in> \<M> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<N> \<and> x \<in> D \<and> D \<subseteq> C"
                and \<N>covered: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>D. D \<in> \<M> \<and> C \<subseteq> D"
     by (blast intro: cell_complex_subdivision_exists [OF \<open>0 < e\<close> \<open>finite \<M>\<close> poly aff_dim_le_DIM face])
@@ -3952,7 +3946,7 @@
   assumes "0 < e" "finite \<M>"
       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
       and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
-      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1"
   obtains \<T> where "triangulation \<T>" "\<And>k. k \<in> \<T> \<Longrightarrow> diameter k < e"
                  "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"