# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1672331576 0
# Node ID 337c2265d8a238325f7691fa5bb0aeffbf5a6957
# Parent  8dac373b92bd4ed7d6d8224845ee897064381a5a
Further cleaning up of messy proofs

diff -r 8dac373b92bd -r 337c2265d8a2 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Dec 29 11:46:32 2022 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Dec 29 16:32:56 2022 +0000
@@ -118,12 +118,7 @@
           have *: "f \<in> U"
             if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
               and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
-          proof -
-            have "Pi\<^sub>E I (Y U) = U"
-              using Y \<open>U \<in> \<U>\<close> by blast
-            then show "f \<in> U"
-              using that unfolding PiE_def Pi_def by blast
-          qed
+            by (smt (verit) PiE_iff Y that)
           show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
             by (auto simp: PiE_iff *)
           show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
@@ -158,18 +153,16 @@
           using Y by force
         show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
           apply clarsimp
-          apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
+          apply (rule_tac x= "(\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
           apply (auto simp: *)
           done
       next
         show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
         proof
           have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
-            apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
-            using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
+            by (simp add: PiE_mono Y \<open>U \<in> \<U>\<close> openin_subset)
           then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
-            using \<open>U \<in> \<U>\<close>
-            by fastforce
+            using \<open>U \<in> \<U>\<close> by fastforce
           moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
             using PiE_mem Y by fastforce
           ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
@@ -211,24 +204,25 @@
   assumes "openin (product_topology T I) U" "x \<in> U"
   shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
 proof -
-  have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
-    using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
-  then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
+  define IT where "IT \<equiv> \<lambda>X. {i. X i \<noteq> topspace (T i)}"
+  have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite (IT X)} U"
+    using assms unfolding product_topology_def IT_def by (intro openin_topology_generated_by) auto
+  then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite (IT X) \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
   proof induction
     case (Int U V x)
     then obtain XU XV where H:
-      "x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"
-      "x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"
-      by auto meson
+      "x \<in> Pi\<^sub>E I XU" "\<And>i. openin (T i) (XU i)" "finite (IT XU)" "Pi\<^sub>E I XU \<subseteq> U"
+      "x \<in> Pi\<^sub>E I XV" "\<And>i. openin (T i) (XV i)" "finite (IT XV)" "Pi\<^sub>E I XV \<subseteq> V"
+      by (meson Int_iff)
     define X where "X = (\<lambda>i. XU i \<inter> XV i)"
     have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
-      unfolding X_def by (auto simp add: PiE_iff)
+      by (auto simp add: PiE_iff X_def)
     then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
     moreover have "\<forall>i. openin (T i) (X i)"
       unfolding X_def using H by auto
-    moreover have "finite {i. X i \<noteq> topspace (T i)}"
-      apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
-      unfolding X_def using H by auto
+    moreover have "finite (IT X)"
+      apply (rule rev_finite_subset[of "IT XU \<union> IT XV"])
+      using H by (auto simp: X_def IT_def)
     moreover have "x \<in> Pi\<^sub>E I X"
       unfolding X_def using H by auto
     ultimately show ?case
@@ -236,16 +230,10 @@
   next
     case (UN K x)
     then obtain k where "k \<in> K" "x \<in> k" by auto
-    with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
-      by simp
-    then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
-      by blast
-    then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
-      using \<open>k \<in> K\<close> by auto
-    then show ?case
-      by auto
+    with \<open>k \<in> K\<close> UN show ?case
+      by (meson Sup_upper2)
   qed auto
-  then show ?thesis using \<open>x \<in> U\<close> by auto
+  then show ?thesis using \<open>x \<in> U\<close> IT_def by blast
 qed
 
 lemma product_topology_empty_discrete:
@@ -257,9 +245,7 @@
     arbitrary union_of
           ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
            relative_to topspace (product_topology X I))"
-  apply (subst product_topology)
-  apply (simp add: topology_inverse' [OF istopology_subbase])
-  done
+  by (simp add: istopology_subbase product_topology)
 
 lemma subtopology_PiE:
   "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
@@ -349,6 +335,7 @@
   "openin (product_topology X I) S \<longleftrightarrow>
     (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
                  (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+sledgehammer [isar_proofs, provers = "cvc4 z3 spass e vampire verit", timeout = 77]
   unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
   apply safe
   apply (drule bspec; blast)+
@@ -438,9 +425,7 @@
 
 corollary closedin_product_topology:
    "closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
-  apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
-  apply (metis closure_of_empty)
-  done
+  by (smt (verit, best) PiE_eq closedin_empty closure_of_eq closure_of_product_topology)
 
 corollary closedin_product_topology_singleton:
    "f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
@@ -501,17 +486,13 @@
   also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
     using * \<open>J \<subseteq> I\<close> by auto
   also have "openin T1 (...)"
-    apply (rule openin_INT)
-    apply (simp add: \<open>finite J\<close>)
-    using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
+    using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast
   ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
 next
-  show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
-    apply (subst topology_generated_by_topspace[symmetric])
-    apply (subst product_topology_def[symmetric])
-    apply (simp only: topspace_product_topology)
-    apply (auto simp add: PiE_iff)
-    using assms unfolding continuous_map_def by auto
+  have "f ` topspace T1 \<subseteq> topspace (product_topology T I)"
+    using assms continuous_map_def by fastforce
+  then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+    by (simp add: product_topology_def)
 qed
 
 lemma continuous_map_product_then_coordinatewise [intro]:
@@ -522,8 +503,7 @@
   fix i assume "i \<in> I"
   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
   also have "continuous_map T1 (T i) (...)"
-    apply (rule continuous_map_compose[of _ "product_topology T I"])
-    using assms \<open>i \<in> I\<close> by auto
+    by (metis \<open>i \<in> I\<close> assms continuous_map_compose continuous_map_product_coordinates)
   ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
     by simp
 next
@@ -583,28 +563,14 @@
   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
   shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
 proof -
-  define J where "J = x`I"
-  define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
-  define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
+  define V where "V \<equiv> (\<lambda>y. if y \<in> x`I then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
+  define X where "X \<equiv> (\<lambda>y. if y \<in> x`I then V y else UNIV)"
   have *: "open (X i)" for i
     unfolding X_def V_def using assms by auto
-  have **: "finite {i. X i \<noteq> UNIV}"
-    unfolding X_def V_def J_def using assms(1) by auto
-  have "open (Pi\<^sub>E UNIV X)"
-    by (simp add: "*" "**" open_PiE)
+  then have "open (Pi\<^sub>E UNIV X)"
+    by (simp add: X_def assms(1) open_PiE)
   moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
-    apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
-    proof (auto)
-      fix f :: "'a \<Rightarrow> 'b" and i :: 'i
-      assume a1: "i \<in> I"
-      assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
-      have f3: "x i \<in> x`I"
-        using a1 by blast
-      have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
-        using a1 by blast
-      then show "f (x i) \<in> U i"
-        using f3 a2 by (meson Inter_iff)
-    qed
+    by (fastforce simp add: PiE_iff X_def V_def split: if_split_asm)
   ultimately show ?thesis by simp
 qed
 
@@ -620,25 +586,13 @@
   fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
   assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
   shows "continuous_on S f"
-  using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
-  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
-
-lemma continuous_on_product_then_coordinatewise_UNIV:
-  assumes "continuous_on UNIV f"
-  shows "continuous_on UNIV (\<lambda>x. f x i)"
-  unfolding continuous_map_iff_continuous2 [symmetric]
-  by (rule continuous_map_product_then_coordinatewise [where I=UNIV]) (use assms in \<open>auto simp: euclidean_product_topology\<close>)
+  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology
+      continuous_map_coordinatewise_then_product)
 
 lemma continuous_on_product_then_coordinatewise:
   assumes "continuous_on S f"
   shows "continuous_on S (\<lambda>x. f x i)"
-proof -
-  have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
-    by (metis assms continuous_on_compose continuous_on_id
-        continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
-  then show ?thesis
-    by auto
-qed
+  by (metis UNIV_I assms continuous_map_iff_continuous continuous_map_product_then_coordinatewise(1) euclidean_product_topology)
 
 lemma continuous_on_coordinatewise_iff:
   fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
@@ -679,16 +633,15 @@
   next
     case (Suc N)
     define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
-      where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
+      where "f = (\<lambda>(x, b). x(N:=b))"
     have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
     proof (auto)
       fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
-      define y where "y = (\<lambda>i. if i = N then a else x i)"
-      have "f (y, x N) = x"
-        unfolding f_def y_def by auto
-      moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
-        unfolding y_def using H \<open>a \<in> F\<close> by auto
-      ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+      have "f (x(N:=a), x N) = x"
+        unfolding f_def by auto
+      moreover have "(x(N:=a), x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
+        using H \<open>a \<in> F\<close> by auto
+      ultimately show "x \<in> f ` ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
         by (metis (no_types, lifting) image_eqI)
     qed
     moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
@@ -742,7 +695,7 @@
     by metis
   text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
   define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
-  have "countable (B i)" for i unfolding B_def by auto
+  have countB: "countable (B i)" for i unfolding B_def by auto
   have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
     by (auto simp: B_def A)
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
@@ -750,14 +703,14 @@
     unfolding K_def B_def by auto
   then have "K \<noteq> {}" by auto
   have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
-    apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
+    by (simp add: countB countable_product_event_const)
   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
     unfolding K_def by auto
   ultimately have "countable K" by auto
-  have "x \<in> k" if "k \<in> K" for k
+  have I: "x \<in> k" if "k \<in> K" for k
     using that unfolding K_def B_def apply auto using A(1) by auto
-  have "open k" if "k \<in> K" for k
-    using that unfolding K_def  by (blast intro: open_B open_PiE elim: )
+  have II: "open k" if "k \<in> K" for k
+    using that unfolding K_def by (blast intro: open_B open_PiE)
   have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
   proof -
     have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
@@ -775,31 +728,28 @@
     have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
       unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
     have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
-      apply (cases "i \<in> I")
-      unfolding Y_def using * that apply (auto)
-      apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
-      unfolding B_def apply simp
-      unfolding I_def apply auto
-      done
+    proof (cases "i \<in> I")
+      case True
+      then show ?thesis  
+        by (metis (mono_tags, lifting) "*" Nitpick.Eps_psimp Y_def)
+    next
+      case False
+      then show ?thesis by (simp add: B_def I_def Y_def)
+    qed
     have "{i. Y i \<noteq> UNIV} \<subseteq> I"
       unfolding Y_def by auto
-    then have ***: "finite {i. Y i \<noteq> UNIV}"
-      unfolding I_def using H(3) rev_finite_subset by blast
-    have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
-      using ** *** by auto
+    with ** have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
+      using H(3) I_def finite_subset by blast
     then have "Pi\<^sub>E UNIV Y \<in> K"
       unfolding K_def by auto
-
     have "Y i \<subseteq> X i" for i
-      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+      using "**" by auto
+    then have "Pi\<^sub>E UNIV Y \<subseteq> U"
+      by (metis H(4) PiE_mono subset_trans)
     then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
   qed
-
   show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
-    apply (rule first_countableI[of K])
-    using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
+    using \<open>countable K\<close> I II Inc by (simp add: first_countableI) 
 qed
 
 proposition product_topology_countable_basis:
@@ -821,7 +771,7 @@
     unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
 
   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
-    apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
+    using \<open>countable B2\<close>  by (intro countable_product_event_const) auto
   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
     unfolding K_def by auto
   ultimately have ii: "countable K" by auto
@@ -832,9 +782,7 @@
     then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
       unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
-    have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
-      by simp
-    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+    obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"
                            "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
@@ -845,29 +793,15 @@
     have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
       unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
     have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
-      using someI_ex[OF *]
-      apply (cases "i \<in> I")
-      unfolding Y_def using * apply (auto)
-      unfolding B2_def I_def by auto
+      using someI_ex[OF *] by (simp add: B2_def I_def Y_def)
     have "{i. Y i \<noteq> UNIV} \<subseteq> I"
       unfolding Y_def by auto
-    then have ***: "finite {i. Y i \<noteq> UNIV}"
-      unfolding I_def using H(3) rev_finite_subset by blast
-    have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
-      using ** *** by auto
+    then have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
+      using "**" H(3) I_def finite_subset by blast
     then have "Pi\<^sub>E UNIV Y \<in> K"
       unfolding K_def by auto
-
-    have "Y i \<subseteq> X i" for i
-      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
-
-    have "x \<in> Pi\<^sub>E UNIV Y"
-      using ** by auto
-
-    show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
-      using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
+    then show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
+      by (meson "**" H(4) PiE_I PiE_mono UNIV_I order.trans)
   next
     fix U assume "U \<in> K"
     show "open U"
@@ -878,9 +812,11 @@
 qed
 
 instance "fun" :: (countable, second_countable_topology) second_countable_topology
-  apply standard
-  using product_topology_countable_basis topological_basis_imp_subbasis by auto
-
+proof
+  show "\<exists>B::('a \<Rightarrow> 'b) set set. countable B \<and> open = generate_topology B"
+    using product_topology_countable_basis topological_basis_imp_subbasis 
+    by auto
+qed
 
 subsection\<open>The Alexander subbase theorem\<close>
 
@@ -1106,11 +1042,7 @@
   qed
   ultimately show ?thesis
     by metis
-next
-  case False
-  then show ?thesis
-    by (auto simp: continuous_map_def PiE_def)
-qed
+qed (auto simp: continuous_map_def PiE_def)
 
 
 lemma continuous_map_componentwise_UNIV:
@@ -1147,8 +1079,7 @@
       fix x f
       assume "f \<in> V"
       let ?T = "{a \<in> topspace(Y i).
-                   (\<lambda>j. if j = i then a
-                        else if j \<in> I then f j else undefined) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
+                   (\<lambda>j\<in>I. f j)(i:=a) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
       show "\<exists>T. openin (Y i) T \<and> f i \<in> T \<and> T \<subseteq> (\<lambda>f. f i) ` V"
       proof (intro exI conjI)
         show "openin (Y i) ?T"
@@ -1164,8 +1095,8 @@
               by simp (metis IntD1 PiE_iff V \<open>f \<in> V\<close> that)
           qed
           then show "continuous_map (Y i) (product_topology Y I)
-                  (\<lambda>x j. if j = i then x else if j \<in> I then f j else undefined)"
-            by (auto simp: continuous_map_componentwise assms extensional_def)
+                  (\<lambda>x. (\<lambda>j\<in>I. f j)(i:=x))"
+            by (auto simp: continuous_map_componentwise assms extensional_def restrict_def)
         next
           have "openin (product_topology Y I) (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
             by (metis openin_topspace topspace_product_topology)
@@ -1177,18 +1108,15 @@
               show "\<And>X. X \<in> (\<inter>) (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) ` \<F> \<Longrightarrow> openin (product_topology Y I) X"
                 unfolding openin_product_topology relative_to_def
                 apply (clarify intro!: arbitrary_union_of_inc)
-                apply (rename_tac F)
-                apply (rule_tac x=F in exI)
                 using subsetD [OF \<F>]
-                apply (force intro: finite_intersection_of_inc)
-                done
+                by (metis (mono_tags, lifting) finite_intersection_of_inc mem_Collect_eq topspace_product_topology)
             qed (use \<open>finite \<F>\<close> \<open>\<F> \<noteq> {}\<close> in auto)
           qed
           ultimately show "openin (product_topology Y I) ((\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>)"
             by (auto simp only: Int_Inter_eq split: if_split)
         qed
       next
-        have eqf: "(\<lambda>j. if j = i then f i else if j \<in> I then f j else undefined) = f"
+        have eqf: "(\<lambda>j\<in>I. f j)(i:=f i) = f"
           using PiE_arb V \<open>f \<in> V\<close> by force
         show "f i \<in> ?T"
           using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
@@ -1273,10 +1201,8 @@
   next
     assume ?rhs
     then show ?lhs
-      apply (simp only: openin_product_topology)
-      apply (rule arbitrary_union_of_inc)
-      apply (auto simp: product_topology_base_alt)
-      done
+      unfolding openin_product_topology
+      by (intro arbitrary_union_of_inc) (auto simp: product_topology_base_alt)
   qed
   ultimately show ?thesis
     by simp
@@ -1306,9 +1232,7 @@
         by (simp add: continuous_map_product_projection)
       moreover
       have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
-        using \<open>i \<in> I\<close> z
-        apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
-        done
+        using \<open>i \<in> I\<close> z by (rule_tac x="z(i:=x)" in image_eqI) auto
       then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
         using \<open>i \<in> I\<close> z by auto
       ultimately show "compactin (X i) (topspace (X i))"
@@ -1461,7 +1385,7 @@
             then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
               using that
               apply (clarsimp simp add: set_eq_iff)
-              apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
+              apply (rule_tac x="f(k:=x)" in image_eqI, auto)
               done
             then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
               using Ceq by auto
@@ -1493,7 +1417,7 @@
               using PiE_ext \<open>g \<in> U\<close> gin by force
           next
             case (insert i M)
-            define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
+            define f where "f \<equiv> h(i:=g i)"
             have fin: "f \<in> PiE I (topspace \<circ> X)"
               unfolding f_def using gin insert.prems(1) by auto
             have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
@@ -1506,13 +1430,13 @@
               show ?thesis
               proof (cases "i \<in> I")
                 case True
-                let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
-                let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
+                let ?U = "{x \<in> topspace(X i). h(i:=x) \<in> U}"
+                let ?V = "{x \<in> topspace(X i). h(i:=x) \<in> V}"
                 have False
                 proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
                   have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
                     using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
-                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
+                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x. h(i:=x))"
                     using \<open>i \<in> I\<close> insert.prems(1)
                     by (auto simp: continuous_map_componentwise extensional_def)
                   show "openin (X i) ?U"
@@ -1522,45 +1446,23 @@
                   show "topspace (X i) \<subseteq> ?U \<union> ?V"
                   proof clarsimp
                     fix x
-                    assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
+                    assume "x \<in> topspace (X i)" and "h(i:=x) \<notin> V"
                     with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
-                    show "(\<lambda>j. if j = i then x else h j) \<in> U"
-                      by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
+                    show "h(i:=x) \<in> U"
+                      by (force dest: subsetD [where c="h(i:=x)"])
                   qed
                   show "?U \<inter> ?V = {}"
                     using disj by blast
                   show "?U \<noteq> {}"
-                    using \<open>U \<noteq> {}\<close> f_def
-                  proof -
-                    have "(\<lambda>j. if j = i then g i else h j) \<in> U"
-                      using \<open>f \<in> U\<close> f_def by blast
-                    moreover have "f i \<in> topspace (X i)"
-                      by (metis PiE_iff True comp_apply fin)
-                    ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
-                      using f_def by auto
-                    then show ?thesis
-                      by blast
-                  qed
-                  have "(\<lambda>j. if j = i then h i else h j) = h"
-                    by force
-                  moreover have "h i \<in> topspace (X i)"
-                    using True insert.prems(1) by auto
-                  ultimately show "?V \<noteq> {}"
-                    using \<open>h \<in> V\<close>  by force
+                    using True \<open>f \<in> U\<close> f_def gin by auto
+                  show "?V \<noteq> {}"
+                    using True \<open>h \<in> V\<close> V openin_subset by fastforce
                 qed
                 then show ?thesis ..
               next
                 case False
                 show ?thesis
-                proof (cases "h = f")
-                  case True
-                  show ?thesis
-                    by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
-                next
-                  case False
-                  then show ?thesis
-                    using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
-                qed
+                  using insert.prems(1) by (metis False gin PiE_E \<open>f \<in> U\<close> f_def fun_upd_triv)
               qed
             next
               case False
@@ -1640,14 +1542,8 @@
   assumes "i \<in> I"
   shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
            (topspace(product_topology X I) = {} \<longrightarrow> topspace(X i) = {})"
-         (is "?lhs = ?rhs")
-proof
-  assume ?lhs with assms show ?rhs
-    by (auto simp: continuous_open_quotient_map open_map_product_projection)
-next
-  assume ?rhs with assms show ?lhs
-    by (auto simp: Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection)
-qed
+  by (metis assms image_empty quotient_imp_surjective_map retraction_imp_quotient_map 
+      retraction_map_product_projection)
 
 lemma product_topology_homeomorphic_component:
   assumes "i \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
@@ -1676,9 +1572,8 @@
     from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" 
       by force
     have "?SX f i homeomorphic_space X i"
-      apply (simp add: subtopology_PiE )
-      using product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
-      using f by fastforce
+      using f product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
+      by (force simp add: subtopology_PiE)
     then show ?thesis
       using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
   qed