# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1742757983 0
# Node ID b022c013b04be2edd232176a5ed67fd2ea1b3ff8
# Parent  3529946fca19c7409cfb26781da7eaf10b8c1e70
Function space instead of image closure

diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -81,13 +81,13 @@
    "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
     \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
   unfolding Euclidean_space_def continuous_map_in_subtopology
-  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_add)
+  by (auto simp: continuous_map_componentwise_UNIV Pi_iff continuous_map_add)
 
 lemma continuous_map_Euclidean_space_diff [continuous_intros]:
    "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
     \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
-  unfolding Euclidean_space_def continuous_map_in_subtopology
-  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)
+  unfolding Euclidean_space_def continuous_map_in_subtopology 
+  by (auto simp: continuous_map_componentwise_UNIV Pi_iff continuous_map_diff)
 
 lemma continuous_map_Euclidean_space_iff:
   "continuous_map (Euclidean_space m) euclidean g
@@ -101,7 +101,7 @@
 next
   assume "continuous_on (topspace (Euclidean_space m)) g"
   then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclidean g"
-    by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space)
+    by (simp add: topspace_Euclidean_space)
   then show "continuous_map (Euclidean_space m) euclidean g"
     by (simp add: Euclidean_space_def euclidean_product_topology)
 qed
@@ -353,7 +353,7 @@
         for k
         unfolding case_prod_unfold o_def
         by (intro continuous_map_into_fulltopology [OF continuous_map_fst] continuous_intros) auto
-      moreover have "?h ` ({0..1} \<times> topspace (nsphere p)) \<subseteq> {x. \<forall>i\<ge>Suc p. x i = 0}"
+      moreover have "?h \<in> ({0..1} \<times> topspace (nsphere p)) \<rightarrow> {x. \<forall>i\<ge>Suc p. x i = 0}"
         using continuous_map_image_subset_topspace [OF f]
         by (auto simp: nsphere image_subset_iff a0)
       moreover have "(\<lambda>i. 0) \<notin> ?h ` ({0..1} \<times> topspace (nsphere p))"
@@ -376,7 +376,8 @@
           using eq unfolding * by (simp add: fun_eq_iff)
       qed
       ultimately show "continuous_map (prod_topology ?T01 (nsphere p)) ?Y ?h"
-        by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV)
+        unfolding Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV 
+        by (force simp flip: image_subset_iff_funcset)
     next
       have *: "\<lbrakk>\<forall>i\<ge>Suc p. x i = 0; x \<noteq> (\<lambda>i. 0)\<rbrakk> \<Longrightarrow> (\<Sum>j\<le>p. (x j)\<^sup>2) \<noteq> 0" for x :: "nat \<Rightarrow> real"
         by (force simp: fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff)
diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -1567,12 +1567,12 @@
     by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq)
 qed
 
-lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
-       (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+lemma continuous_map_subset_aux1: 
+  "continuous_map X Y f \<Longrightarrow> (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
   using continuous_map_image_closure_subset by blast
 
 lemma continuous_map_subset_aux2:
-  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
+  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S"
   shows "continuous_map X Y f"
   unfolding continuous_map_closedin
 proof (intro conjI ballI allI impI)
@@ -1598,18 +1598,18 @@
 qed
 
 lemma continuous_map_eq_image_closure_subset:
-     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
 
 lemma continuous_map_eq_image_closure_subset_alt:
-     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
 
 lemma continuous_map_eq_image_closure_subset_gen:
      "continuous_map X Y f \<longleftrightarrow>
         f \<in> topspace X \<rightarrow> topspace Y \<and>
-        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
-  by (meson Pi_iff continuous_map continuous_map_eq_image_closure_subset image_subset_iff)
+        (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
+  by (metis continuous_map_eq_image_closure_subset continuous_map_funspace)
 
 lemma continuous_map_closure_preimage_subset:
    "continuous_map X Y f
@@ -1697,16 +1697,18 @@
   by (auto simp: elim!: continuous_map_eq)
 
 lemma continuous_map_in_subtopology:
-  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
+  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f \<in> (topspace X) \<rightarrow> S"
   (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   show ?rhs
   proof -
-    have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
-      by (meson L continuous_map_image_closure_subset)
+    have "\<And>A. f \<in> (X closure_of A) \<rightarrow> subtopology X' S closure_of f ` A"
+      by (metis L continuous_map_eq_image_closure_subset image_subset_iff_funcset)
     then show ?thesis
-      by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset order.trans)
+      by (metis closure_of_subset_subtopology closure_of_subtopology_subset
+          closure_of_topspace continuous_map_eq_image_closure_subset
+          image_subset_iff_funcset subset_trans)
   qed
 next
   assume R: ?rhs
@@ -3963,7 +3965,7 @@
 proof
   show "?lhs \<Longrightarrow> ?rhs"
     unfolding embedding_map_def
-    by (metis continuous_map_in_subtopology homeomorphic_imp_continuous_map inf_absorb2 subtopology_subtopology)
+    by (metis Int_subset_iff homeomorphic_imp_surjective_map inf_le1 subtopology_restrict subtopology_subtopology topspace_subtopology)
 qed (simp add: embedding_map_def inf.absorb_iff2 subtopology_subtopology)
 
 lemma injective_open_imp_embedding_map:
@@ -4118,13 +4120,13 @@
   using assms continuous_on_closed by blast
 
 lemma continuous_map_subtopology_eu [simp]:
-  "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+  "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h \<in> S \<rightarrow> T"
   by (simp add: continuous_map_in_subtopology)
 
 lemma continuous_map_euclidean_top_of_set:
   assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f"
   shows "continuous_map euclidean (top_of_set S) f"
-  by (simp add: cont continuous_map_in_subtopology eq image_subset_iff_subset_vimage)
+  using cont continuous_map_iff_continuous2 continuous_map_into_subtopology eq by blast
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Half-global and completely global cases\<close>
@@ -4166,25 +4168,14 @@
   by (metis Int_commute closedin_closed continuous_on_closed_invariant)
 
 lemma continuous_open_preimage:
-  assumes contf: "continuous_on S f" and "open S" "open T"
+  assumes "continuous_on S f" and "open S" "open T"
   shows "open (S \<inter> f -` T)"
-proof-
-  obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
-    using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
-    unfolding openin_open by auto
-  then show ?thesis
-    using open_Int[of S U, OF \<open>open S\<close>] by auto
-qed
+  by (metis Int_commute assms continuous_on_open_vimage)
 
 lemma continuous_closed_preimage:
-  assumes contf: "continuous_on S f" and "closed S" "closed T"
+  assumes "continuous_on S f" and "closed S" "closed T"
   shows "closed (S \<inter> f -` T)"
-proof-
-  obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
-    using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
-    unfolding closedin_closed by auto
-  then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
-qed
+  by (metis assms closed_vimage_Int inf_commute)
 
 lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
   by (metis continuous_on_eq_continuous_within open_vimage) 
diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -97,12 +97,23 @@
   by (metis locally_compact_closedin closedin_retract)
 
 lemma homotopic_into_retract:
-   "\<lbrakk>f \<in> S \<rightarrow> T; g \<in> S \<rightarrow> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
-        \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
-  apply (subst (asm) homotopic_with_def)
-  apply (simp add: homotopic_with retract_of_def retraction_def Pi_iff, clarify)
-  apply (rule_tac x="r \<circ> h" in exI)
-  by (smt (verit, ccfv_SIG) comp_def continuous_on_compose continuous_on_subset image_subset_iff)
+  assumes fg: "f \<in> S \<rightarrow> T" "g \<in> S \<rightarrow> T"
+  assumes "T retract_of U"
+  assumes "homotopic_with_canon (\<lambda>x. True) S U f g"
+  shows "homotopic_with_canon (\<lambda>x. True) S T f g"
+proof -
+  obtain h r where r: "retraction U T r"
+     "continuous_on ({0..1::real} \<times> S) h"
+      and h: "h \<in> {0..1} \<times> S \<rightarrow> U \<and> (\<forall>x. h (0, x) = f x) \<and> (\<forall>x. h (1, x) = g x)"
+    using assms by (auto simp: homotopic_with_def retract_of_def)
+  then have "continuous_on ({0..1} \<times> S) (r \<circ> h)"
+    by (metis continuous_on_compose continuous_on_subset funcset_image
+        retraction_def)
+  then show ?thesis
+    using r fg h
+    apply (simp add: retraction homotopic_with Pi_iff)
+    by (smt (verit, best) imageI)
+qed
 
 lemma retract_of_locally_connected:
   assumes "locally connected T" "S retract_of T"
@@ -131,7 +142,8 @@
   ultimately
   show ?thesis
     unfolding homotopy_equivalent_space_def
-    by (smt (verit, del_insts) continuous_map_id continuous_map_subtopology_eu id_def r retraction retraction_comp subset_refl) 
+    by (meson continuous_map_from_subtopology_mono continuous_map_id
+        continuous_map_subtopology_eu r retraction_def)
 qed
 
 lemma deformation_retract:
@@ -2235,7 +2247,7 @@
   have "continuous_on ({0..1} \<times> S) h"
     unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs)
   moreover
-  have "h ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
+  have "h \<in> ({0..1} \<times> S) \<rightarrow> sphere 0 1"
     unfolding h_def using g  by (auto simp: divide_simps path_defs)
   ultimately show ?thesis
     using g by (auto simp: h_def path_defs homotopic_with_def)
diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -2743,7 +2743,8 @@
       by (auto simp: Arg2pi_ge_0 Arg2pi_lt_2pi less_imp_le)
     also have "... \<subseteq> S"
       using him by blast
-    finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+    finally show "(\<lambda>w. h (fst w, Arg2pi (snd w) / (2 * pi))) \<in> {0..1} \<times> sphere 0 1 \<rightarrow> S"
+      by blast 
   qed (auto simp: h0 h1)
 qed
 
diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Homotopy.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -116,21 +116,21 @@
     by (cases "t = 1") (simp_all add: assms)
 qed auto
 
+lemma homotopic_with_imp_funspace1:
+     "homotopic_with_canon P X Y f g \<Longrightarrow> f \<in> X \<rightarrow> Y"
+  using homotopic_with_imp_continuous_maps by fastforce
+
 lemma homotopic_with_imp_subset1:
      "homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
-  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+  using homotopic_with_imp_funspace1 by blast
+
+lemma homotopic_with_imp_funspace2:
+     "homotopic_with_canon P X Y f g \<Longrightarrow> g \<in> X \<rightarrow> Y"
+  using homotopic_with_imp_continuous_maps by force
 
 lemma homotopic_with_imp_subset2:
      "homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
-  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
-
-lemma homotopic_with_imp_funspace1:
-     "homotopic_with_canon P X Y f g \<Longrightarrow> f \<in> X \<rightarrow> Y"
-  using homotopic_with_imp_subset1 by blast
-
-lemma homotopic_with_imp_funspace2:
-     "homotopic_with_canon P X Y f g \<Longrightarrow> g \<in> X \<rightarrow> Y"
-  using homotopic_with_imp_subset2 by blast
+  using homotopic_with_imp_funspace2 by blast
 
 lemma homotopic_with_subset_left:
      "\<lbrakk>homotopic_with_canon P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with_canon P Z Y f g"
@@ -485,10 +485,11 @@
 
 lemma homotopic_paths_imp_subset:
      "homotopic_paths S p q \<Longrightarrow> path_image p \<subseteq> S \<and> path_image q \<subseteq> S"
-  by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)
+  by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2
+      path_image_def)
 
 proposition homotopic_paths_refl [simp]: "homotopic_paths S p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> S"
-  by (simp add: homotopic_paths_def path_def path_image_def)
+  by (auto simp add: homotopic_paths_def path_def path_image_def)
 
 proposition homotopic_paths_sym: "homotopic_paths S p q \<Longrightarrow> homotopic_paths S q p"
   by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
@@ -684,7 +685,7 @@
 lemma homotopic_loops:
    "homotopic_loops S p q \<longleftrightarrow>
       (\<exists>h. continuous_on ({0..1::real} \<times> {0..1}) h \<and>
-          image h ({0..1} \<times> {0..1}) \<subseteq> S \<and>
+          h \<in> ({0..1} \<times> {0..1}) \<rightarrow> S \<and>
           (\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
           (\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
           (\<forall>t \<in> {0..1}. pathfinish(h \<circ> Pair t) = pathstart(h \<circ> Pair t)))"
@@ -702,12 +703,13 @@
 proposition homotopic_loops_imp_subset:
      "homotopic_loops S p q \<Longrightarrow> path_image p \<subseteq> S \<and> path_image q \<subseteq> S"
   unfolding homotopic_loops_def path_image_def
-  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+  by (simp add: homotopic_with_imp_subset1 homotopic_with_imp_subset2)
 
 proposition homotopic_loops_refl:
      "homotopic_loops S p p \<longleftrightarrow>
       path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p"
-  by (simp add: homotopic_loops_def path_image_def path_def)
+  by (metis (mono_tags, lifting) homotopic_loops_def homotopic_paths_def
+      homotopic_paths_refl homotopic_with_refl)
 
 proposition homotopic_loops_sym: "homotopic_loops S p q \<Longrightarrow> homotopic_loops S q p"
   by (simp add: homotopic_loops_def homotopic_with_sym)
@@ -726,8 +728,9 @@
 proposition homotopic_loops_eq:
    "\<lbrakk>path p; path_image p \<subseteq> S; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
           \<Longrightarrow> homotopic_loops S p q"
-  unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def
-  by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]])
+  unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def image_subset_iff_funcset
+  using homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]]
+  by fastforce
 
 proposition homotopic_loops_continuous_image:
    "\<lbrakk>homotopic_loops S f g; continuous_on S h; h \<in> S \<rightarrow> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
@@ -1247,7 +1250,7 @@
       using p1 p2 unfolding homotopic_loops
       apply clarify
       subgoal for h k
-        by (rule_tac x="\<lambda>z. (h z, k z)" in exI) (force intro: continuous_intros simp: path_defs)
+        by (rule_tac x="\<lambda>z. (h z, k z)" in exI) (auto intro: continuous_intros simp: path_defs)
       done
   qed
   with assms show ?thesis
@@ -3786,7 +3789,9 @@
 
 lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
   unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
-  by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology)
+  apply (erule ex_forward)+
+  by (metis continuous_map_subtopology_eu homotopic_with_id2 openin_imp_subset openin_subtopology_self topspace_euclidean_subtopology
+      image_subset_iff_funcset)
 
 lemma homotopy_eqv_inj_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -3963,7 +3968,8 @@
   shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}" (is "?lhs = ?rhs")
 proof
   assume ?lhs then show ?rhs
-    by (metis continuous_map_subtopology_eu empty_iff equalityI homotopy_equivalent_space_def image_subset_iff subsetI)
+    by (meson continuous_map_subtopology_eu equals0D equals0I funcset_mem
+        homotopy_equivalent_space_def)
 qed (use homeomorphic_imp_homotopy_eqv in force)
 
 lemma homotopy_eqv_empty2 [simp]:
@@ -5281,8 +5287,8 @@
     assume c: "homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
     then have contf: "continuous_on (sphere a r) f" 
       by (metis homotopic_with_imp_continuous)
-    moreover have fim: "f ` sphere a r \<subseteq> S"
-      by (meson continuous_map_subtopology_eu c homotopic_with_imp_continuous_maps)
+    moreover have fim: "f \<in> sphere a r \<rightarrow> S"
+      using homotopic_with_imp_subset1 that by blast
     show ?P
       using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
   qed
@@ -5373,7 +5379,7 @@
         by (intro continuous_intros)
       qed (auto simp: dist_norm norm_minus_commute mult_left_le_one_le)
     moreover
-    have "?h ` ({0..1} \<times> sphere a r) \<subseteq> S"
+    have "?h \<in> ({0..1} \<times> sphere a r) \<rightarrow> S"
       by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD])
     moreover
     have "\<forall>x\<in>sphere a r. ?h (0, x) = g a" "\<forall>x\<in>sphere a r. ?h (1, x) = f x"
diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Retracts.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -1815,7 +1815,7 @@
         apply (intro continuous_on_compose continuous_intros)
         apply (force intro: inV continuous_on_subset [OF contk] continuous_on_subset [OF conta])+
         done
-      show "(k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) ` ({0..1} \<times> T) \<subseteq> U"
+      show "(k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) \<in> ({0..1} \<times> T) \<rightarrow> U"
         using inV kim by auto
       show "\<forall>x\<in>T. (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) (0, x) = f x"
         by (simp add: B_def h'_def keq)
@@ -2211,7 +2211,7 @@
   proof (simp add: homotopic_with, intro exI conjI)
     show "continuous_on ({0..1} \<times> T') k"
       using TW continuous_on_subset contk by auto
-    show "k ` ({0..1} \<times> T') \<subseteq> U"
+    show "k \<in> ({0..1} \<times> T') \<rightarrow> U"
       using TW kim by fastforce
     have "T' \<subseteq> S"
       by (meson opeT' subsetD openin_imp_subset)
@@ -2246,7 +2246,7 @@
                   and hom: "\<And>n. homotopic_with_canon (\<lambda>x. True) (V n) T f g"
       using assms by auto 
     then obtain h where conth: "\<And>n. continuous_on ({0..1::real} \<times> V n) (h n)"
-                  and him: "\<And>n. h n ` ({0..1} \<times> V n) \<subseteq> T" 
+                  and him: "\<And>n. h n \<in> ({0..1} \<times> V n) \<rightarrow> T" 
                   and h0: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (0, x) = f x" 
                   and h1: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (1, x) = g x"
       by (simp add: homotopic_with) metis
@@ -2277,7 +2277,7 @@
     proof (simp add: homotopic_with eqU [symmetric], intro exI conjI ballI)
       show "continuous_on ({0..1} \<times> \<Union>\<V>) \<zeta>"
         using V eqU by (blast intro!:  continuous_on_subset [OF cont])
-      show "\<zeta>` ({0..1} \<times> \<Union>\<V>) \<subseteq> T"
+      show "\<zeta> \<in> ({0..1} \<times> \<Union>\<V>) \<rightarrow> T"
       proof clarsimp
         fix t :: real and y :: "'a" and X :: "'a set"
         assume "y \<in> X" "X \<in> \<V>" and t: "0 \<le> t" "t \<le> 1"
diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Urysohn.thy
--- a/src/HOL/Analysis/Urysohn.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Urysohn.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -45,7 +45,7 @@
     then show ?thesis
        by (auto simp: f_def cInf_lower)
   qed
-  ultimately have fim: "f ` topspace X \<subseteq> {0..1}"
+  ultimately have fim: "f \<in> topspace X \<rightarrow> {0..1}"
     by (auto simp: f_def)
   have 0: "0 \<in> dyadics \<inter> {0..1::real}" and 1: "1 \<in> dyadics \<inter> {0..1::real}"
     by (force simp: dyadics_def)+
@@ -161,17 +161,17 @@
     qed
   qed
   then have contf: "continuous_map X (top_of_set {0..1}) f"
-    by (force simp: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: mtopology_is_euclidean)
+    by (auto simp: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim abs_minus_commute simp flip: mtopology_is_euclidean)
   define g where "g \<equiv> \<lambda>x. a + (b - a) * f x"
   show thesis
   proof
     have "continuous_map X euclideanreal g"
       using contf \<open>a \<le> b\<close> unfolding g_def by (auto simp: continuous_intros continuous_map_in_subtopology)
-    moreover have "g ` (topspace X) \<subseteq> {a..b}"
-      using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close>   
-      by (simp add: g_def add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq)
+    moreover have "g \<in> (topspace X) \<rightarrow> {a..b}"
+      using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close> 
+      by (simp add: g_def Pi_iff add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq)
     ultimately show "continuous_map X (top_of_set {a..b}) g"
-      by (meson continuous_map_in_subtopology)
+      using continuous_map_in_subtopology by blast
     show "g ` S \<subseteq> {a}" "g ` T \<subseteq> {b}"
       using fimS fimT by (auto simp: g_def)
   qed
@@ -576,8 +576,8 @@
       where conth: "continuous_map X (top_of_set {0..1}) h" 
             and him: "h ` W \<subseteq> {0}" "h ` S \<subseteq> {1}"
       by (metis XS normal_space_iff_Urysohn) 
-    then have him01: "h ` topspace X \<subseteq> {0..1}"
-      by (meson continuous_map_in_subtopology)
+    then have him01: "h \<in> topspace X \<rightarrow> {0..1}"
+      by (metis continuous_map_in_subtopology)
     obtain z where "z \<in> T"
       using \<open>T \<noteq> {}\<close> by blast
     define g' where "g' \<equiv> \<lambda>x. z + h x * (g x - z)"
@@ -1066,7 +1066,7 @@
 proof -
   have *: "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
     if contf: "continuous_map X euclideanreal f" and a: "a \<in> topspace X - C" and "closedin X C"
-      and fim: "f ` topspace X \<subseteq> {0..1}" and f0: "f a = 0" and f1: "f ` C \<subseteq> {1}"
+      and fim: "f \<in> topspace X \<rightarrow> {0..1}" and f0: "f a = 0" and f1: "f ` C \<subseteq> {1}"
     for C a f
   proof (intro exI conjI)
     show "openin X {x \<in> topspace X. f x \<in> {..<1 / 2}}" "openin X {x \<in> topspace X. f x \<in> {1 / 2<..}}"
@@ -1078,9 +1078,9 @@
       using \<open>closedin X C\<close> f1 closedin_subset by auto
   qed (auto simp: disjnt_iff)
   show ?thesis
-    using assms
+    using assms *
     unfolding completely_regular_space_def regular_space_def continuous_map_in_subtopology
-    by (meson "*")
+    by metis
 qed
 
 
@@ -4028,11 +4028,11 @@
     have "closedin X {x}"
       by (simp add: \<open>Hausdorff_space X\<close> closedin_Hausdorff_singleton \<open>x \<in> topspace X\<close>)
     then obtain f where contf: "continuous_map X euclideanreal f" 
-      and f01: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> {0..1}" and fxy: "f y = 0" "f x = 1"
-      using \<open>completely_regular_space X\<close> xy unfolding completely_regular_space_def
-      by (smt (verit, ccfv_threshold) Diff_iff continuous_map_in_subtopology image_subset_iff singleton_iff)
+      and f01: "f \<in> topspace X \<rightarrow> {0..1}" and fxy: "f y = 0" "f x = 1"
+      using \<open>completely_regular_space X\<close> xy unfolding completely_regular_space_def Pi_iff continuous_map_in_subtopology image_subset_iff
+      by (metis Diff_iff empty_iff insert_iff)
     then have "bounded (f ` topspace X)"
-      by (meson bounded_closed_interval bounded_subset image_subset_iff)
+      by (metis bounded_closed_interval bounded_subset image_subset_iff_funcset)
     with contf f01 have "restrict f (topspace X) \<in> K"
       by (auto simp: K_def)
     with fxy xy show ?thesis 
@@ -4047,11 +4047,13 @@
     fix x U
     assume "e x \<in> K \<rightarrow>\<^sub>E {0..1}" and "x \<in> topspace X" and "openin X U" and "x \<in> U"
     then obtain g where contg: "continuous_map X (top_of_set {0..1}) g" and "g x = 0" 
-          and gim: "g ` (topspace X - U) \<subseteq> {1::real}"
+          and gim: "g \<in> (topspace X - U) \<rightarrow> {1::real}"
       using \<open>completely_regular_space X\<close> unfolding completely_regular_space_def 
-      by (metis Diff_iff openin_closedin_eq)
+      using Diff_iff openin_closedin_eq
+      by (metis image_subset_iff_funcset)
     then have "bounded (g ` topspace X)"
-      by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology)
+      by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology
+          image_subset_iff_funcset)
     moreover have "g \<in> topspace X \<rightarrow> {0..1}"
       using contg by (simp add: continuous_map_def)
     ultimately have g_in_K: "restrict g (topspace X) \<in> K"
@@ -4067,7 +4069,7 @@
       have "e y (restrict g (topspace X)) \<in> {0..<1}"
         using ey by (smt (verit, ccfv_SIG) PiE_mem g_in_K)
     with gim g_in_K y \<open>y \<notin> U\<close> show ?thesis
-      by (fastforce simp: e_def)
+      by (fastforce simp: e_def Pi_iff)
     qed
     ultimately
     show "\<exists>W. openin (product_topology (\<lambda>f. top_of_set {0..1}) K) W \<and> e x \<in> W \<and> e' ` (e ` topspace X \<inter> W - {e x}) \<subseteq> U"
@@ -4120,7 +4122,7 @@
                   and g1: "\<And>t. t \<in> T \<Longrightarrow> g t ` S \<subseteq> {1}"
       by metis
     then have g01: "\<And>t. t \<in> T \<Longrightarrow> g t ` topspace X \<subseteq> {0..1}"
-      by (meson continuous_map_in_subtopology)
+      by (meson continuous_map_in_subtopology image_subset_iff_funcset)
     define G where "G \<equiv> \<lambda>t. {x \<in> topspace X. g t x \<in> {..<1/2}}"
     have "Ball (G`T) (openin X)"
       using contg unfolding G_def continuous_map_in_subtopology
@@ -4171,11 +4173,12 @@
   define g where "g \<equiv> \<lambda>x. a + (b - a) * f x"
   show thesis
   proof
-    have "\<forall>x\<in>topspace X. a + (b - a) * f x \<le> b"
-      using contf \<open>a \<le> b\<close> apply (simp add: continuous_map_in_subtopology image_subset_iff)
-      by (smt (verit, best) mult_right_le_one_le)
+    have "a + (b - a) * f i \<le> b" if "i \<in> topspace X" for i
+      using that contf \<open>a \<le> b\<close> affine_ineq [of "f i" a b]
+      unfolding continuous_map_in_subtopology continuous_map_upper_lower_semicontinuous_le_gen Pi_iff 
+      by (simp add: algebra_simps)
     then show "continuous_map X (top_of_set {a..b}) g"
-      using contf \<open>a \<le> b\<close> unfolding g_def continuous_map_in_subtopology image_subset_iff
+      using contf \<open>a \<le> b\<close> unfolding g_def continuous_map_in_subtopology Pi_iff
       by (intro conjI continuous_intros; simp)
     show "g ` T \<subseteq> {a}" "g ` S \<subseteq> {b}"
       using f0 f1 by (auto simp: g_def)
@@ -4193,7 +4196,7 @@
   show thesis
   proof
     show "continuous_map X (top_of_set {a..b}) (uminus \<circ> f)"
-      using contf by (auto simp: continuous_map_in_subtopology o_def)
+      using contf by (auto simp: continuous_map_in_subtopology o_def Pi_iff)
     show "(uminus o f) ` T \<subseteq> {a}" "(uminus o f) ` S \<subseteq> {b}"
       using fim by fastforce+
   qed
@@ -4256,7 +4259,7 @@
     proof
       show "continuous_map (subtopology cube (e ` S)) X e'"
         by (meson \<open>compactin X S\<close> compactin_subset_topspace conte' continuous_map_from_subtopology_mono image_mono)
-      show "e' ` topspace (subtopology cube (e ` S)) \<subseteq> S"
+      show "e' \<in> topspace (subtopology cube (e ` S)) \<rightarrow> S"
         using \<open>compactin X S\<close> compactin_subset_topspace e'e by fastforce
     qed
   qed (simp add: contf)
diff -r 3529946fca19 -r b022c013b04b src/HOL/Homology/Brouwer_Degree.thy
--- a/src/HOL/Homology/Brouwer_Degree.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Homology/Brouwer_Degree.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -96,7 +96,7 @@
    "hom_boundary p X S
   \<in> hom (relative_homology_group p X S) (reduced_homology_group (p-1) (subtopology X S))"
 proof -
-  have *: "continuous_map X (discrete_topology {()}) (\<lambda>x. ())" "(\<lambda>x. ()) ` S \<subseteq> {()}"
+  have *: "continuous_map X (discrete_topology {()}) (\<lambda>x. ())" "(\<lambda>x. ()) \<in> S \<rightarrow> {()}"
     by auto
   interpret group_hom "relative_homology_group p (discrete_topology {()}) {()}"
                       "homology_group (p-1) (discrete_topology {()})"
@@ -435,33 +435,34 @@
 
 
 lemma deformation_retraction_relative_homology_group_isomorphisms:
-   "\<lbrakk>retraction_maps X Y r s; r ` U \<subseteq> V; s ` V \<subseteq> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
+   "\<lbrakk>retraction_maps X Y r s; r \<in> U \<rightarrow> V; s \<in> V \<rightarrow> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
     \<Longrightarrow> group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V)
              (hom_induced p X U Y V r) (hom_induced p Y V X U s)"
   apply (simp add: retraction_maps_def)
   apply (rule homotopy_equivalence_relative_homology_group_isomorphisms)
-       apply (auto simp: image_subset_iff continuous_map_compose homotopic_with_equal)
+       apply (auto simp: image_subset_iff_funcset Pi_iff continuous_map_compose homotopic_with_equal)
   done
 
 
 lemma deformation_retract_relative_homology_group_isomorphisms:
-   "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+   "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
         \<Longrightarrow> group_isomorphisms (relative_homology_group p X U) (relative_homology_group p Y V)
              (hom_induced p X U Y V r) (hom_induced p Y V X U id)"
-  by (simp add: deformation_retraction_relative_homology_group_isomorphisms)
+  by (simp add: deformation_retraction_relative_homology_group_isomorphisms
+      in_mono)
 
 lemma deformation_retract_relative_homology_group_isomorphism:
-   "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+   "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
     \<Longrightarrow> (hom_induced p X U Y V r) \<in> iso (relative_homology_group p X U) (relative_homology_group p Y V)"
   by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso)
 
 lemma deformation_retract_relative_homology_group_isomorphism_id:
-   "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+   "\<lbrakk>retraction_maps X Y r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
     \<Longrightarrow> (hom_induced p Y V X U id) \<in> iso (relative_homology_group p Y V) (relative_homology_group p X U)"
   by (metis deformation_retract_relative_homology_group_isomorphisms group_isomorphisms_imp_iso group_isomorphisms_sym)
 
 lemma deformation_retraction_imp_isomorphic_relative_homology_groups:
-   "\<lbrakk>retraction_maps X Y r s; r ` U \<subseteq> V; s ` V \<subseteq> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
+   "\<lbrakk>retraction_maps X Y r s; r \<in> U \<rightarrow> V; s ` V \<subseteq> U; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X (s \<circ> r) id\<rbrakk>
     \<Longrightarrow> relative_homology_group p X U \<cong> relative_homology_group p Y V"
   by (blast intro: is_isoI group_isomorphisms_imp_iso deformation_retraction_relative_homology_group_isomorphisms)
 
@@ -471,7 +472,7 @@
   by (simp add: deformation_retraction_imp_homotopy_equivalent_space homotopy_equivalent_space_imp_isomorphic_homology_groups)
 
 lemma deformation_retract_imp_isomorphic_relative_homology_groups:
-   "\<lbrakk>retraction_maps X X' r id; V \<subseteq> U; r ` U \<subseteq> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
+   "\<lbrakk>retraction_maps X X' r id; V \<subseteq> U; r \<in> U \<rightarrow> V; homotopic_with (\<lambda>h. h ` U \<subseteq> U) X X r id\<rbrakk>
         \<Longrightarrow> relative_homology_group p X U \<cong> relative_homology_group p X' V"
   by (simp add: deformation_retraction_imp_isomorphic_relative_homology_groups)
 
@@ -482,7 +483,7 @@
 
 
 lemma epi_hom_induced_inclusion:
-  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
   shows "(hom_induced p (subtopology X S) {} X {} id)
    \<in> epi (homology_group p (subtopology X S)) (homology_group p X)"
 proof (rule epi_right_invertible)
@@ -493,14 +494,20 @@
       \<in> carrier (homology_group p X) \<rightarrow> carrier (homology_group p (subtopology X S))"
     by (simp add: hom_induced_carrier)
   fix x
-  assume "x \<in> carrier (homology_group p X)"
-  then show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f x) = x"
-    by (metis  assms continuous_map_id_subt continuous_map_in_subtopology hom_induced_compose' hom_induced_id homology_homotopy_empty homotopic_with_imp_continuous_maps image_empty order_refl)
+  assume x: "x \<in> carrier (homology_group p X)"
+  show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f x) = x"
+  proof (subst hom_induced_compose')
+    show "continuous_map X (subtopology X S) f"
+      by (meson assms continuous_map_into_subtopology
+          homotopic_with_imp_continuous_maps)
+    show "hom_induced p X {} X {} (id \<circ> f) x = x"
+      by (metis assms(1) hom_induced_id homology_homotopy_empty id_comp x)
+  qed (use assms in auto)
 qed
 
 
 lemma trivial_homomorphism_hom_induced_relativization:
-  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
   shows "trivial_homomorphism (homology_group p X) (relative_homology_group p X S)
               (hom_induced p X {} X S id)"
 proof -
@@ -514,7 +521,7 @@
 
 
 lemma mon_hom_boundary_inclusion:
-  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
   shows "(hom_boundary p X S) \<in> mon
              (relative_homology_group p X S) (homology_group (p - 1) (subtopology X S))"
 proof -
@@ -528,7 +535,7 @@
 qed
 
 lemma short_exact_sequence_hom_induced_relativization:
-  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
   shows "short_exact_sequence (homology_group (p-1) X) (homology_group (p-1) (subtopology X S)) (relative_homology_group p X S)
                    (hom_induced (p-1) (subtopology X S) {} X {} id) (hom_boundary p X S)"
   unfolding short_exact_sequence_iff
@@ -537,7 +544,7 @@
 
 lemma group_isomorphisms_homology_group_prod_deformation:
   fixes p::int
-  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
   obtains H K where
     "subgroup H (homology_group p (subtopology X S))"
     "subgroup K (homology_group p (subtopology X S))"
@@ -561,15 +568,19 @@
   have x: "short_exact_sequence (?pX) ?pXS ?rhs ?hi ?hb"
     using short_exact_sequence_hom_induced_relativization [OF assms, of "p + 1"] by simp
   have contf: "continuous_map X (subtopology X S) f"
-    by (meson assms continuous_map_in_subtopology homotopic_with_imp_continuous_maps)
+    by (metis assms continuous_map_into_subtopology homotopic_with_imp_continuous_maps)
   obtain H K where HK: "H \<lhd> ?pXS" "subgroup K ?pXS" "H \<inter> K \<subseteq> {one ?pXS}" "set_mult ?pXS H K = carrier ?pXS"
     and iso: "?hb \<in> iso ?rhs (subgroup_generated ?pXS H)" "?hi \<in> iso (subgroup_generated ?pXS K) ?pX"
-    apply (rule splitting_lemma_right [OF x, where g' = "hom_induced p X {} (subtopology X S) {} f"])
-      apply (simp add: hom_induced_empty_hom)
-     apply (simp add: contf hom_induced_compose')
-     apply (metis (full_types) assms(1) hom_induced_id homology_homotopy_empty)
-    apply blast
-    done
+  proof (rule splitting_lemma_right [OF x, where g' = "hom_induced p X {} (subtopology X S) {} f"])
+    show "hom_induced p X {} (subtopology X S) {} f \<in> hom (homology_group p X) (homology_group p (subtopology X S))"
+      using hom_induced_empty_hom by blast
+  next
+    fix z 
+    assume "z \<in> carrier (homology_group p X)"
+    then show "hom_induced p (subtopology X S) {} X {} id (hom_induced p X {} (subtopology X S) {} f z) = z"
+      using assms(1) contf hom_induced_id homology_homotopy_empty
+      by (fastforce simp add: hom_induced_compose')
+  qed blast
   show ?thesis
   proof
     show "subgroup H ?pXS"
@@ -587,7 +598,7 @@
 qed
 
 lemma iso_homology_group_prod_deformation:
-  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  assumes "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
   shows "homology_group p (subtopology X S)
       \<cong> DirProd (homology_group p X) (relative_homology_group(p + 1) X S)"
     (is "?G \<cong> DirProd ?H ?R")
@@ -613,7 +624,7 @@
   assumes "contractible_space X" "S \<subseteq> topspace X" "S \<noteq> {}"
   shows  "homology_group  0 (subtopology X S) \<cong> DirProd integer_group (relative_homology_group(1) X S)"
 proof -
-  obtain f where  "homotopic_with (\<lambda>x. True) X X id f" and "f ` (topspace X) \<subseteq> S"
+  obtain f where  "homotopic_with (\<lambda>x. True) X X id f" and "f \<in> topspace X \<rightarrow> S"
     using assms contractible_space_alt by fastforce
   then have "homology_group 0 (subtopology X S) \<cong> homology_group 0 X \<times>\<times> relative_homology_group 1 X S"
     using iso_homology_group_prod_deformation [of X _ S 0] by auto
@@ -911,7 +922,8 @@
   qed
   ultimately
   have cmh: "continuous_map (prod_topology ?T01 ?X12) (nsphere n) h"
-    by (subst (2) nsphere) (simp add: continuous_map_in_subtopology continuous_map_componentwise_UNIV)
+  proof (subst (2) nsphere) 
+  qed (fastforce simp add: continuous_map_in_subtopology continuous_map_componentwise_UNIV)
   have "hom_induced p (subtopology (nsphere n) {x. 0 \<le> x k})
              (topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}) ?X12
              (topspace ?X12 \<inter> {x. - 1/2 \<le> x k \<and> x k \<le> 0}) id
@@ -928,13 +940,13 @@
           apply (auto simp: h_def Let_def)
         done
       show "continuous_map (subtopology (nsphere n) {x. 0 \<le> x k}) ?X12 id"
-        by (simp add: continuous_map_in_subtopology) (auto simp: nsphere)
+        by (simp add: continuous_map_in_subtopology)
     qed (simp add: nsphere h)
   next
     have h0: "\<And>xa. \<lbrakk>xa \<in> topspace (nsphere n); - (1/2) \<le> xa k; xa k \<le> 0\<rbrakk> \<Longrightarrow> h (0, xa) k = 0"
       by (simp add: h_def Let_def)
-    show "(h \<circ> (\<lambda>x. (0,x))) ` (topspace ?X12 \<inter> {x. - 1 / 2 \<le> x k \<and> x k \<le> 0})
-        \<subseteq> topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
+    show "(h \<circ> (\<lambda>x. (0,x))) \<in> (topspace ?X12 \<inter> {x. - 1 / 2 \<le> x k \<and> x k \<le> 0})
+        \<rightarrow> topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
       apply (auto simp: h0)
       apply (rule subsetD [OF continuous_map_image_subset_topspace [OF cmh]])
       apply (force simp: nsphere)
@@ -981,9 +993,8 @@
     by (simp add: nsphere if_distrib [of "\<lambda>x. x ^ 2"] cong: if_cong)
   show ?thesis
     unfolding n
-    apply (rule iso_relative_homology_of_contractible [where p = "1 + p", simplified])
-    using contractible_space_upper_hemisphere ne apply blast+
-    done
+    using iso_relative_homology_of_contractible [where p = "1 + p", simplified]
+    by (metis contractible_space_upper_hemisphere dual_order.refl empty_iff ne)
 qed
 
 corollary iso_reduced_homology_group_upper_hemisphere:
@@ -1090,10 +1101,8 @@
   "\<lbrakk>\<exists>f \<in> iso G1 G2. \<forall>x \<in> carrier G1. r2(f x) = f(r1 x); \<exists>f \<in> iso G2 G3. \<forall>x \<in> carrier G2. r3(f x) = f(r2 x)\<rbrakk>
    \<Longrightarrow> \<exists>f \<in> iso G1 G3. \<forall>x \<in> carrier G1. r3(f x) = f(r1 x)"
   apply clarify
-  apply (rename_tac g f)
-  apply (rule_tac x="f \<circ> g" in bexI)
-  apply (metis iso_iff comp_apply hom_in_carrier)
-  using iso_set_trans by blast
+  by (smt (verit, ccfv_threshold) Group.iso_iff hom_in_carrier iso_set_trans
+      o_apply)
 
 lemma reduced_homology_group_nsphere_step:
    "\<exists>f \<in> iso(reduced_homology_group p (nsphere n))
@@ -1106,7 +1115,9 @@
   define r where "r \<equiv> \<lambda>x::nat\<Rightarrow>real. \<lambda>i. if i = 0 then -x i else x i"
   have cmr: "continuous_map (nsphere n) (nsphere n) r" for n
     unfolding r_def by (rule continuous_map_nsphere_reflection)
-  have rsub: "r ` {x. 0 \<le> x (Suc n)} \<subseteq> {x. 0 \<le> x (Suc n)}" "r ` {x. x (Suc n) \<le> 0} \<subseteq> {x. x (Suc n) \<le> 0}" "r ` {x. x (Suc n) = 0} \<subseteq> {x. x (Suc n) = 0}"
+  have rsub: "r \<in> {x. 0 \<le> x (Suc n)} \<rightarrow> {x. 0 \<le> x (Suc n)}" 
+             "r \<in> {x. x (Suc n) \<le> 0} \<rightarrow> {x. x (Suc n) \<le> 0}" 
+             "r \<in> {x. x (Suc n) = 0} \<rightarrow> {x. x (Suc n) = 0}"
     by (force simp: r_def)+
   let ?sub = "subtopology (nsphere (Suc n)) {x. x (Suc n) \<ge> 0}"
   let ?G2 = "relative_homology_group (1 + p) ?sub {x. x (Suc n) = 0}"
@@ -1126,12 +1137,13 @@
       fix c
       assume "c \<in> carrier ?G2"
       have cmrs: "continuous_map ?sub ?sub r"
-        by (metis (mono_tags, lifting) IntE cmr continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff rsub(1) topspace_subtopology)
+        by (metis (no_types, lifting) IntE Pi_iff cmr continuous_map_from_subtopology
+            continuous_map_into_subtopology rsub(1) topspace_subtopology)
       have "hom_induced p (nsphere n) {} (nsphere n) {} r \<circ> hom_boundary (1 + p) ?sub {x. x (Suc n) = 0}
           = hom_boundary (1 + p) ?sub {x. x (Suc n) = 0} \<circ>
             hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r"
         using naturality_hom_induced [OF cmrs rsub(3), symmetric, of "1+p", simplified]
-        by (simp add: subtopology_subtopology subtopology_nsphere_equator flip: Collect_conj_eq cong: rev_conj_cong)
+        by (simp add: Pi_iff subtopology_subtopology subtopology_nsphere_equator flip: Collect_conj_eq cong: rev_conj_cong)
       then show "?j p n (?f c) = ?f (hom_induced (1 + p) ?sub {x. x (Suc n) = 0} ?sub {x. x (Suc n) = 0} r c)"
         by (metis comp_def)
     next
@@ -1199,12 +1211,11 @@
     then show ?thesis
       by (simp add: nsphere)
   qed
-  have *: "reduced_homology_group p (subtopology (powertop_real UNIV) {?a, ?b}) \<cong>
+  have "t1_space (powertop_real UNIV)"
+    using t1_space_euclidean t1_space_product_topology by blast
+  then have *: "reduced_homology_group p (subtopology (powertop_real UNIV) {?a, ?b}) \<cong>
         homology_group p (subtopology (powertop_real UNIV) {?a})"
-    apply (rule reduced_homology_group_pair)
-      apply (simp_all add: fun_eq_iff)
-    apply (simp add: open_fun_def separation_t1 t1_space_def)
-    done
+    by (intro reduced_homology_group_pair) (auto simp: fun_eq_iff)
   have "reduced_homology_group 0 (nsphere 0) \<cong> integer_group" if "p=0"
   proof -
     have "reduced_homology_group 0 (nsphere 0) \<cong> homology_group 0 (top_of_set {?a})" if "p=0"
@@ -1352,9 +1363,9 @@
     and aeq: "subgroup_generated ?G {a} = ?G"
     using cyclic_reduced_homology_group_nsphere [of p p] by (auto simp: cyclic_group_def)
   show ?thesis
-    using hi [OF a]
-    apply (simp add: Brouwer_degree2 a)
-    by (metis Brouwer_degree2_iff a aeq f group.trivial_group_subgroup_generated group_reduced_homology_group subsetI trivial_reduced_homology_group_nsphere)
+    using hi [OF a] unfolding Brouwer_degree2 a
+    by (metis Brouwer_degree2_iff a aeq f group.trivial_group_subgroup_generated
+        group_reduced_homology_group subsetI trivial_reduced_homology_group_nsphere)
 qed
 
 lemma Brouwer_degree2_unique_generator:
@@ -1487,7 +1498,7 @@
     then have he: "hom_induced p (nsphere p) {} (nsphere p) {} (\<lambda>x. a)
                  = hom_induced p (subtopology (nsphere p) {a}) {} (nsphere p) {} id \<circ>
                    hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (\<lambda>x. a)"
-      by (metis continuous_map_id_subt hom_induced_compose id_comp image_empty order_refl)
+      by (metis continuous_map_id_subt fun.map_id hom_induced_compose_empty)
     have 1: "hom_induced p (nsphere p) {} (subtopology (nsphere p) {a}) {} (\<lambda>x. a) c =
              \<one>\<^bsub>reduced_homology_group (int p) (subtopology (nsphere p) {a})\<^esub>"
       using c trivial_reduced_homology_group_contractible_space [of "subtopology (nsphere p) {a}" p]
@@ -1586,11 +1597,12 @@
     obtain d d' where d: "d \<in> carrier ?P" and d': "d' \<in> carrier ?N" and eqc: "?f(d,d') = c"
       using c by (force simp flip: fim)
     let ?h = "\<lambda>xx. hom_induced 0 (subtopology (nsphere 0) {xx}) {} (discrete_topology {()}) {} (\<lambda>x. ())"
-    have "retraction_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r"
-      apply (simp add: retraction_map_def retraction_maps_def continuous_map_in_subtopology continuous_map_from_subtopology cmr image_subset_iff)
-      apply (rule_tac x=r in exI)
-      apply (force simp: retraction_map_def retraction_maps_def continuous_map_in_subtopology continuous_map_from_subtopology cmr)
-      done
+    have "continuous_map (subtopology (nsphere 0) {nn}) (nsphere 0) r"
+      using cmr continuous_map_from_subtopology by blast
+    then have "retraction_map (subtopology (nsphere 0) {pp}) (subtopology (nsphere 0) {nn}) r"
+      apply (simp add: retraction_map_def retraction_maps_def continuous_map_in_subtopology)
+      using \<open>r nn = pp\<close> \<open>r pp = nn\<close> cmr continuous_map_from_subtopology
+      by blast
     then have "carrier ?N = (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r) ` carrier ?P"
       by (rule surj_hom_induced_retraction_map)
     then obtain e where e: "e \<in> carrier ?P" and eqd': "hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r e = d'"
diff -r 3529946fca19 -r b022c013b04b src/HOL/Homology/Homology_Groups.thy
--- a/src/HOL/Homology/Homology_Groups.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Homology/Homology_Groups.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -379,19 +379,19 @@
   by (metis hom_boundary)+
 
 lemma hom_chain_map:
-   "\<lbrakk>continuous_map X Y f; f ` S \<subseteq> T\<rbrakk>
+   "\<lbrakk>continuous_map X Y f; f \<in> S \<rightarrow> T\<rbrakk>
         \<Longrightarrow> (chain_map p f) \<in> hom (relcycle_group p X S) (relcycle_group p Y T)"
-  by (force simp: chain_map_add singular_relcycle_chain_map hom_def)
+  by (simp add: chain_map_add hom_def singular_relcycle_chain_map)
 
 
 lemma hom_induced1:
   "\<exists>hom_relmap.
     (\<forall>p X S Y T f.
-        continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T
+        continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T
         \<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group (int p) X S)
                                (relative_homology_group (int p) Y T)) \<and>
     (\<forall>p X S Y T f c.
-        continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+        continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
         singular_relcycle p X S c
         \<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
             homologous_rel_set p Y T (chain_map p f c))"
@@ -399,7 +399,7 @@
   have "\<exists>y. (y \<in> hom (relative_homology_group (int p) X S) (relative_homology_group (int p) Y T)) \<and>
            (\<forall>c. singular_relcycle p X S c \<longrightarrow>
                 y (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c))"
-    if contf: "continuous_map X Y f" and fim: "f ` (topspace X \<inter> S) \<subseteq> T"
+    if contf: "continuous_map X Y f" and fim: "f \<in> (topspace X \<inter> S) \<rightarrow> T"
     for p X S Y T and f :: "'a \<Rightarrow> 'b"
   proof -
     let ?f = "(#>\<^bsub>relcycle_group p Y T\<^esub>) (singular_relboundary_set p Y T) \<circ> chain_map p f"
@@ -441,12 +441,12 @@
     "\<exists>hom_relmap.
       (\<forall>p X S Y T f.
           continuous_map X Y f \<and>
-          f ` (topspace X \<inter> S) \<subseteq> T
+          f \<in> (topspace X \<inter> S) \<rightarrow> T
           \<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group p X S)
                                  (relative_homology_group p Y T)) \<and>
       (\<forall>p X S Y T f c.
           continuous_map X Y f \<and>
-          f ` (topspace X \<inter> S) \<subseteq> T \<and>
+          f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
           singular_relcycle p X S c
           \<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
               homologous_rel_set p Y T (chain_map p f c)) \<and>
@@ -464,13 +464,13 @@
 lemma hom_induced3:
   "\<exists>hom_relmap.
     ((\<forall>p X S Y T f c.
-        ~(continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+        ~(continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
           c \<in> carrier(relative_homology_group p X S))
         \<longrightarrow> hom_relmap p X S Y T f c = one(relative_homology_group p Y T)) \<and>
     (\<forall>p X S Y T f.
         hom_relmap p X S Y T f \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)) \<and>
     (\<forall>p X S Y T f c.
-        continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> singular_relcycle p X S c
+        continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> singular_relcycle p X S c
         \<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
             homologous_rel_set p Y T (chain_map p f c)) \<and>
     (\<forall>p X S Y T.
@@ -486,24 +486,24 @@
   moreover have "\<exists>x. ?P x \<and> ?Q x"
   proof -
     obtain hom_relmap:: "[int,'a topology,'a set,'b topology,'b set,'a \<Rightarrow> 'b,('a chain) set] \<Rightarrow> ('b chain) set"
-      where 1: "\<And>p X S Y T f. \<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T\<rbrakk> \<Longrightarrow>
+      where 1: "\<And>p X S Y T f. \<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T\<rbrakk> \<Longrightarrow>
                    hom_relmap p X S Y T f
                    \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)"
         and 2: "\<And>p X S Y T f c.
-                   \<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+                   \<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
                    \<Longrightarrow>
                    hom_relmap (int p) X S Y T f (homologous_rel_set p X S c) =
                    homologous_rel_set p Y T (chain_map p f c)"
         and 3: "(\<forall>p. p < 0 \<longrightarrow> hom_relmap p = (\<lambda>X S Y T f c. undefined))"
       using hom_induced2 [where ?'a='a and ?'b='b]
-      by (metis (mono_tags, lifting))
-    have 4: "\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; c \<in> carrier (relative_homology_group p X S)\<rbrakk> \<Longrightarrow>
+      by (fastforce simp: Pi_iff)
+    have 4: "\<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; c \<in> carrier (relative_homology_group p X S)\<rbrakk> \<Longrightarrow>
         hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
            \<in> carrier (relative_homology_group p Y T)"
       for p X S Y f T c
       using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]] 
             continuous_map_image_subset_topspace by fastforce
-    have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+    have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
                       c \<in> carrier (relative_homology_group p X S)
             then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
             else \<one>\<^bsub>relative_homology_group p Y T\<^esub>)
@@ -522,16 +522,16 @@
         show ?thesis
         proof (cases "continuous_map X Y f")
           case True
-          then have "f ` (topspace X \<inter> S) \<subseteq> topspace Y"
+          then have "f \<in> (topspace X \<inter> S) \<rightarrow> topspace Y"
             using continuous_map_image_subset_topspace by blast
           then show ?thesis
             using True False that
             using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
-          by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
+            by (simp add: 4 Pi_iff continuous_map_funspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
         qed (simp add: group.is_monoid)
       qed
     qed
-    have hrel: "\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+    have hrel: "\<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
             \<Longrightarrow> hom_relmap (int p) X (topspace X \<inter> S) Y (topspace Y \<inter> T)
               f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
         for p X S Y T f c
@@ -539,13 +539,14 @@
             continuous_map_image_subset_topspace by fastforce
     show ?thesis
       apply (rule_tac x="\<lambda>p X S Y T f c.
-               if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
+               if continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
                   c \<in> carrier(relative_homology_group p X S)
                then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
                else one(relative_homology_group p Y T)" in exI)
       apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
-          group.is_monoid group.restrict_hom_iff 4 inhom hrel cong: if_cong)
-      apply (force simp: continuous_map_def intro!: ext)
+          group.is_monoid group.restrict_hom_iff 4 inhom hrel split: if_splits)
+      apply (intro ext strip)
+      apply (auto simp: continuous_map_def)
       done
   qed
   ultimately show ?thesis
@@ -558,7 +559,7 @@
   hom_induced:
     "((\<forall>p X S Y T f c.
         ~(continuous_map X Y f \<and>
-          f ` (topspace X \<inter> S) \<subseteq> T \<and>
+          f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
           c \<in> carrier(relative_homology_group p X S))
         \<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f c =
             one(relative_homology_group p Y T)) \<and>
@@ -567,7 +568,7 @@
                            (relative_homology_group p Y T)) \<and>
     (\<forall>p X S Y T f c.
         continuous_map X Y f \<and>
-        f ` (topspace X \<inter> S) \<subseteq> T \<and>
+        f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
         singular_relcycle p X S c
         \<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f (homologous_rel_set p X S c) =
             homologous_rel_set p Y T (chain_map p f c)) \<and>
@@ -581,7 +582,7 @@
   by (fact hom_induced3)
 
 lemma hom_induced_default:
-    "~(continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> c \<in> carrier(relative_homology_group p X S))
+    "~(continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> c \<in> carrier(relative_homology_group p X S))
           \<Longrightarrow> hom_induced p X S Y T f c = one(relative_homology_group p Y T)"
   and hom_induced_hom:
     "hom_induced p X S Y T f \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)"
@@ -593,15 +594,15 @@
   by (metis hom_induced)+
 
 lemma hom_induced_chain_map_gen:
-  "\<lbrakk>continuous_map X Y f; f ` (topspace X \<inter> S) \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+  "\<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
   \<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
   by (metis hom_induced)
 
 lemma hom_induced_chain_map:
-   "\<lbrakk>continuous_map X Y f; f ` S \<subseteq> T; singular_relcycle p X S c\<rbrakk>
+   "\<lbrakk>continuous_map X Y f; f \<in> S \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
     \<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c)
       = homologous_rel_set p Y T (chain_map p f c)"
-  by (meson Int_lower2 hom_induced image_subsetI image_subset_iff subset_iff)
+  by (simp add: Pi_iff hom_induced_chain_map_gen)
 
 
 lemma hom_induced_eq:
@@ -619,10 +620,11 @@
     case 2
     have "hom_induced n X S Y T f C = hom_induced n X S Y T g C" for C
     proof -
-      have "continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and> C \<in> carrier (relative_homology_group n X S)
-        \<longleftrightarrow> continuous_map X Y g \<and> g ` (topspace X \<inter> S) \<subseteq> T \<and> C \<in> carrier (relative_homology_group n X S)"
+      have "continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> C \<in> carrier (relative_homology_group n X S)
+        \<longleftrightarrow> continuous_map X Y g \<and> g \<in> (topspace X \<inter> S) \<rightarrow> T \<and> C \<in> carrier (relative_homology_group n X S)"
         (is "?P = ?Q")
-        by (metis IntD1 assms continuous_map_eq image_cong)
+        using assms Pi_iff continuous_map_eq [of X Y]
+        by (smt (verit, ccfv_SIG) Int_iff)
       then consider "\<not> ?P \<and> \<not> ?Q" | "?P \<and> ?Q"
         by blast
       then show ?thesis
@@ -633,18 +635,18 @@
       next
         case 2
         have "homologous_rel_set n Y T (chain_map n f c) = homologous_rel_set n Y T (chain_map n g c)"
-          if "continuous_map X Y f" "f ` (topspace X \<inter> S) \<subseteq> T"
-             "continuous_map X Y g" "g ` (topspace X \<inter> S) \<subseteq> T"
+          if "continuous_map X Y f" "f \<in> (topspace X \<inter> S) \<rightarrow> T"
+             "continuous_map X Y g" "g \<in> (topspace X \<inter> S) \<rightarrow> T"
              "C = homologous_rel_set n X S c" "singular_relcycle n X S c"
           for c
         proof -
           have "chain_map n f c = chain_map n g c"
-            using assms chain_map_eq singular_relcycle that by blast
+            using assms chain_map_eq singular_relcycle that by metis
           then show ?thesis
             by simp
         qed
         with 2 show ?thesis
-          by (auto simp: relative_homology_group_def carrier_FactGroup
+          by (force simp: relative_homology_group_def carrier_FactGroup
               right_coset_singular_relboundary hom_induced_chain_map_gen)
       qed
     qed
@@ -705,7 +707,7 @@
   by (rule hom_induced_id_gen) auto
 
 lemma hom_induced_compose:
-  assumes "continuous_map X Y f" "f ` S \<subseteq> T" "continuous_map Y Z g" "g ` T \<subseteq> U"
+  assumes "continuous_map X Y f" "f \<in> S \<rightarrow> T" "continuous_map Y Z g" "g \<in> T \<rightarrow> U"
   shows "hom_induced p X S Z U (g \<circ> f) = hom_induced p Y T Z U g \<circ> hom_induced p X S Y T f"
 proof -
   consider (neg) "p < 0" | (int) n where "p = int n"
@@ -715,7 +717,7 @@
     case int
     have gf: "continuous_map X Z (g \<circ> f)"
       using assms continuous_map_compose by fastforce
-    have gfim: "(g \<circ> f) ` S \<subseteq> U"
+    have gfim: "(g \<circ> f) \<in> S \<rightarrow> U"
       unfolding o_def using assms by blast
     have sr: "\<And>a. singular_relcycle n X S a \<Longrightarrow> singular_relcycle n Y T (chain_map n f a)"
       by (simp add: assms singular_relcycle_chain_map)
@@ -727,7 +729,8 @@
         case True
         with gfim show ?thesis
           unfolding int
-          by (auto simp: carrier_relative_homology_group gf gfim assms sr chain_map_compose  hom_induced_chain_map)
+          by (auto simp: carrier_relative_homology_group gf gfim assms
+              sr chain_map_compose hom_induced_chain_map)
       next
         case False
         then show ?thesis
@@ -738,12 +741,12 @@
 qed
 
 lemma hom_induced_compose':
-  assumes "continuous_map X Y f" "f ` S \<subseteq> T" "continuous_map Y Z g" "g ` T \<subseteq> U"
+  assumes "continuous_map X Y f" "f \<in> S \<rightarrow> T" "continuous_map Y Z g" "g \<in> T \<rightarrow> U"
   shows "hom_induced p Y T Z U g (hom_induced p X S Y T f x) = hom_induced p X S Z U (g \<circ> f) x"
   using hom_induced_compose [OF assms] by simp
 
 lemma naturality_hom_induced:
-  assumes "continuous_map X Y f" "f ` S \<subseteq> T"
+  assumes "continuous_map X Y f" "f \<in> S \<rightarrow> T"
   shows "hom_boundary q Y T \<circ> hom_induced q X S Y T f
        = hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f \<circ> hom_boundary q X S"
 proof (cases "q \<le> 0")
@@ -767,7 +770,7 @@
         using p1 by auto
       have cbm: "(chain_boundary p (chain_map p f a))
                = (chain_map (p - Suc 0) f (chain_boundary p a))"
-        using a chain_boundary_chain_map singular_relcycle by blast
+        using a chain_boundary_chain_map singular_relcycle by metis
       have contf: "continuous_map (subtopology X S) (subtopology Y T) f"
         using assms
         by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
@@ -838,8 +841,9 @@
     \<Longrightarrow> f ` A = f ` B" for f A B
           by blast
         have "?lhs = homologous_rel_set (Suc n) X S ` singular_relcycle_set (Suc n) X {}"
-          using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle 
-          by (smt (verit) bot.extremum comp_apply continuous_map_id image_cong image_empty mem_Collect_eq)
+          using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle
+          by (smt (verit, best) comp_apply continuous_map_id empty_iff funcsetI
+              image_cong mem_Collect_eq) 
         also have "\<dots> = homologous_rel_set (Suc n) X S `
                          (singular_relcycle_set (Suc n) X S \<inter>
                           {c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)})"
@@ -849,7 +853,9 @@
           then show "\<exists>y. y \<in> singular_relcycle_set (Suc n) X S \<inter>
                          {c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)} \<and>
                     homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
-            using singular_cycle singular_relcycle by (fastforce simp: singular_boundary)
+            using singular_cycle singular_relcycle
+            by (metis Int_Collect mem_Collect_eq singular_chain_0
+                singular_relboundary_0)
         next
           fix c
           assume c: "c \<in> singular_relcycle_set (Suc n) X S \<inter>
@@ -956,15 +962,21 @@
     have 2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> f x = f y; \<And>x. x \<in> B \<Longrightarrow> \<exists>y. y \<in> A \<and> f x = f y\<rbrakk>
     \<Longrightarrow> f ` A = f ` B" for f A B
       by blast
-    have "?lhs = homologous_rel_set n X {} ` (singular_relcycle_set n (subtopology X S) {})"
-      by (smt (verit) chain_map_ident continuous_map_id_subt empty_subsetI hom_induced_chain_map image_cong image_empty image_image mem_Collect_eq singular_relcycle)
+    have "\<And>f. singular_chain n (subtopology X S) f \<and>
+         singular_chain (n - Suc 0) trivial_topology (chain_boundary n f) \<Longrightarrow>
+         hom_induced (int n) (subtopology X S) {} X {} id (homologous_rel_set n (subtopology X S) {} f) =
+         homologous_rel_set n X {} f"
+      by (auto simp: chain_map_ident hom_induced_chain_map singular_relcycle)
+    then have "?lhs = homologous_rel_set n X {} ` (singular_relcycle_set n (subtopology X S) {})"
+      by (simp add: singular_relcycle image_comp)
     also have "\<dots> = homologous_rel_set n X {} ` (singular_relcycle_set n X {} \<inter> singular_relboundary_set n X S)"
     proof (rule 2)
       fix c
       assume "c \<in> singular_relcycle_set n (subtopology X S) {}"
       then show "\<exists>y. y \<in> singular_relcycle_set n X {} \<inter> singular_relboundary_set n X S \<and>
             homologous_rel_set n X {} c = homologous_rel_set n X {} y"
-        using singular_chain_imp_relboundary singular_cycle singular_relboundary_imp_chain singular_relcycle by fastforce
+        using singular_chain_imp_relboundary singular_relboundary_imp_chain
+        by (fastforce simp: singular_cycle)
     next
       fix c
       assume "c \<in> singular_relcycle_set n X {} \<inter> singular_relboundary_set n X S"
@@ -1031,7 +1043,7 @@
 
 
 proposition homology_homotopy_axiom:
-  assumes "homotopic_with (\<lambda>h. h ` S \<subseteq> T) X Y f g"
+  assumes "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> T) X Y f g"
   shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
 proof (cases "p < 0")
   case True
@@ -1043,7 +1055,7 @@
     by (metis int_nat_eq not_le)
   have cont: "continuous_map X Y f" "continuous_map X Y g"
     using assms homotopic_with_imp_continuous_maps by blast+
-  have im: "f ` (topspace X \<inter> S) \<subseteq> T" "g ` (topspace X \<inter> S) \<subseteq> T"
+  have im: "f \<in> (topspace X \<inter> S) \<rightarrow> T" "g \<in> (topspace X \<inter> S) \<rightarrow> T"
     using homotopic_with_imp_property assms by blast+
   show ?thesis
   proof
@@ -1073,7 +1085,7 @@
   then obtain n where peq: "p = int n"
     by (metis int_nat_eq not_le)
   have cont: "continuous_map (subtopology X (S - U)) (subtopology X S) id"
-    by (simp add: closure_of_subtopology_mono continuous_map_eq_image_closure_subset)
+    by (meson Diff_subset continuous_map_from_subtopology_mono continuous_map_id)
   have TU: "topspace X \<inter> (S - U) \<inter> (T - U) \<subseteq> T"
     by auto
   show ?thesis
@@ -1090,9 +1102,9 @@
                    (homologous_rel_set n (subtopology X (S - U)) (T - U) c)
                = hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
                    (homologous_rel_set n (subtopology X (S - U)) (T - U) d)"
-      then have scc: "singular_chain n (subtopology X (S - U)) c"
+      then obtain scc: "singular_chain n (subtopology X (S - U)) c"
            and  scd: "singular_chain n (subtopology X (S - U)) d"
-        using singular_relcycle by blast+
+        using singular_relcycle by metis
       have "singular_relboundary n (subtopology X (S - U)) (T - U) c"
         if srb: "singular_relboundary n (subtopology X S) T c"
           and src: "singular_relcycle n (subtopology X (S - U)) (T - U) c" for c
@@ -1167,7 +1179,8 @@
                           "homologous_rel n (subtopology X S) T a c'"
         using a by (blast intro: excised_relcycle_exists [OF assms])
       then have scc': "singular_chain n (subtopology X S) c'"
-        using homologous_rel_singular_chain singular_relcycle that by blast
+        using homologous_rel_singular_chain that
+        by (force simp: singular_relcycle)
       then show ?thesis
         using scc' chain_map_ident [of _ "subtopology X S"] c' homologous_rel_set_eq
         by fastforce
@@ -1182,7 +1195,7 @@
           homologous_rel_set n (subtopology X (S - U)) (T - U) `
           singular_relcycle_set n (subtopology X (S - U)) (T - U)
         = homologous_rel_set n (subtopology X S) T ` singular_relcycle_set n (subtopology X S) T"
-      by (simp add: image_comp o_def hom_induced_chain_map_gen cont TU topspace_subtopology
+      by (simp add: image_comp o_def hom_induced_chain_map_gen cont TU
                        cong: image_cong_simp)
   qed
 qed
@@ -1776,10 +1789,10 @@
   by (simp add: homology_homotopy_axiom)
 
 lemma homotopy_equivalence_relative_homology_group_isomorphisms:
-  assumes contf: "continuous_map X Y f" and fim: "f ` S \<subseteq> T"
-      and contg: "continuous_map Y X g" and gim: "g ` T \<subseteq> S"
-      and gf: "homotopic_with (\<lambda>h. h ` S \<subseteq> S) X X (g \<circ> f) id"
-      and fg: "homotopic_with (\<lambda>k. k ` T \<subseteq> T) Y Y (f \<circ> g) id"
+  assumes contf: "continuous_map X Y f" and fim: "f \<in> S \<rightarrow> T"
+      and contg: "continuous_map Y X g" and gim: "g \<in> T \<rightarrow> S"
+      and gf: "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> S) X X (g \<circ> f) id"
+      and fg: "homotopic_with (\<lambda>k. k \<in> T \<rightarrow> T) Y Y (f \<circ> g) id"
     shows "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T)
                 (hom_induced p X S Y T f) (hom_induced p Y T X S g)"
   unfolding group_isomorphisms_def
@@ -1799,10 +1812,10 @@
 
 
 lemma homotopy_equivalence_relative_homology_group_isomorphism:
-  assumes "continuous_map X Y f" and fim: "f ` S \<subseteq> T"
-      and "continuous_map Y X g" and gim: "g ` T \<subseteq> S"
-      and "homotopic_with (\<lambda>h. h ` S \<subseteq> S) X X (g \<circ> f) id"
-      and "homotopic_with (\<lambda>k. k ` T \<subseteq> T) Y Y (f \<circ> g) id"
+  assumes "continuous_map X Y f" and fim: "f \<in> S \<rightarrow> T"
+      and "continuous_map Y X g" and gim: "g \<in> T \<rightarrow> S"
+      and "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> S) X X (g \<circ> f) id"
+      and "homotopic_with (\<lambda>k. k \<in> T \<rightarrow> T) Y Y (f \<circ> g) id"
     shows "(hom_induced p X S Y T f) \<in> iso (relative_homology_group p X S) (relative_homology_group p Y T)"
   using homotopy_equivalence_relative_homology_group_isomorphisms [OF assms] group_isomorphisms_imp_iso
   by metis
@@ -1816,10 +1829,10 @@
   using assms by (intro homotopy_equivalence_relative_homology_group_isomorphism) auto
 
 lemma homotopy_equivalent_space_imp_isomorphic_relative_homology_groups:
-  assumes "continuous_map X Y f" and fim: "f ` S \<subseteq> T"
-      and "continuous_map Y X g" and gim: "g ` T \<subseteq> S"
-      and "homotopic_with (\<lambda>h. h ` S \<subseteq> S) X X (g \<circ> f) id"
-      and "homotopic_with (\<lambda>k. k ` T \<subseteq> T) Y Y (f \<circ> g) id"
+  assumes "continuous_map X Y f" and fim: "f \<in> S \<rightarrow> T"
+      and "continuous_map Y X g" and gim: "g \<in> T \<rightarrow> S"
+      and "homotopic_with (\<lambda>h. h \<in> S \<rightarrow> S) X X (g \<circ> f) id"
+      and "homotopic_with (\<lambda>k. k \<in> T \<rightarrow> T) Y Y (f \<circ> g) id"
     shows "relative_homology_group p X S \<cong> relative_homology_group p Y T"
   using homotopy_equivalence_relative_homology_group_isomorphism [OF assms]
   unfolding is_iso_def by blast
@@ -1871,7 +1884,7 @@
   by (simp add: trivial_relative_homology_group_empty)
 
 lemma homeomorphic_maps_relative_homology_group_isomorphisms:
-  assumes "homeomorphic_maps X Y f g" and im: "f ` S \<subseteq> T" "g ` T \<subseteq> S"
+  assumes "homeomorphic_maps X Y f g" and im: "f \<in> S \<rightarrow> T" "g \<in> T \<rightarrow> S"
   shows "group_isomorphisms (relative_homology_group p X S) (relative_homology_group p Y T)
                             (hom_induced p X S Y T f) (hom_induced p Y T X S g)"
 proof -
@@ -1884,10 +1897,10 @@
          (hom_induced p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f)
          (hom_induced p Y (topspace Y \<inter> T) X (topspace X \<inter> S) g)"
   proof (rule homotopy_equivalence_relative_homology_group_isomorphisms)
-    show "homotopic_with (\<lambda>h. h ` (topspace X \<inter> S) \<subseteq> topspace X \<inter> S) X X (g \<circ> f) id"
+    show "homotopic_with (\<lambda>h. h \<in> (topspace X \<inter> S) \<rightarrow> topspace X \<inter> S) X X (g \<circ> f) id"
       using fg im by (auto intro: homotopic_with_equal continuous_map_compose)
   next
-    show "homotopic_with (\<lambda>k. k ` (topspace Y \<inter> T) \<subseteq> topspace Y \<inter> T) Y Y (f \<circ> g) id"
+    show "homotopic_with (\<lambda>k. k \<in> (topspace Y \<inter> T) \<rightarrow> topspace Y \<inter> T) Y Y (f \<circ> g) id"
       using fg im by (auto intro: homotopic_with_equal continuous_map_compose)
   qed (use im fg in \<open>auto simp: continuous_map_def\<close>)
   then show ?thesis
@@ -2197,21 +2210,23 @@
   by (simp add: ext hom_boundary_carrier hom_induced_id hom_relboundary_def)
 
 lemma naturality_hom_induced_relboundary:
-  assumes "continuous_map X Y f" "f ` S \<subseteq> U" "f ` T \<subseteq> V"
+  assumes "continuous_map X Y f" "f \<in> S \<rightarrow> U" "f \<in> T \<rightarrow> V"
   shows "hom_relboundary p Y U V \<circ>
          hom_induced p X S Y (U) f =
          hom_induced (p-1) (subtopology X S) T (subtopology Y U) V f \<circ>
          hom_relboundary p X S T"
 proof -
   have [simp]: "continuous_map (subtopology X S) (subtopology Y U) f"
-    using assms continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce
+    using assms continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology
+    by (fastforce simp: Pi_iff)
   have "hom_induced (p-1) (subtopology Y U) {} (subtopology Y U) V id \<circ>
         hom_induced (p-1) (subtopology X S) {} (subtopology Y U) {} f
       = hom_induced (p-1) (subtopology X S) T (subtopology Y U) V f \<circ>
         hom_induced (p-1) (subtopology X S) {} (subtopology X S) T id"
     using assms by (simp flip: hom_induced_compose)
   with assms show ?thesis
-    by (metis (no_types, lifting) fun.map_comp hom_relboundary_def naturality_hom_induced)
+    unfolding hom_relboundary_def 
+    by (metis (no_types, lifting) ext fun.map_comp naturality_hom_induced)
 qed
 
 proposition homology_exactness_triple_1:
@@ -2222,7 +2237,7 @@
                     [hom_relboundary p X S T, hom_induced p X T X S id])"
     (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
 proof -
-  have iTS: "id ` T \<subseteq> S" and [simp]: "S \<inter> T = T"
+  have iTS: "id \<in> T \<rightarrow> S" and [simp]: "S \<inter> T = T"
     using assms by auto
   have "?h2 B \<in> kernel ?G2 ?G1 ?h1" for B
   proof -
@@ -2291,7 +2306,7 @@
       interpret comm_group "?G2"
         by (rule abelian_relative_homology_group)
       have "hom_induced p X T X S id (hom_induced p X {} X T id W) = hom_induced p X {} X S id W"
-        by (simp add: assms hom_induced_compose')
+        using assms iTS by (simp add: hom_induced_compose')
       then have "B = (?h2 \<circ> hom_induced p X {} X T id) W \<otimes>\<^bsub>?G2\<^esub> ?h2 D"
         by (simp add: Bcarr Weq hb.G.m_assoc hom_induced_carrier)
       then show "B = ?h2 ?W"
@@ -2314,14 +2329,14 @@
     (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
 proof -
   let ?H2 = "homology_group (p-1) (subtopology X S)"
-  have iTS: "id ` T \<subseteq> S" and [simp]: "S \<inter> T = T"
+  have iTS: "id \<in> T \<rightarrow> S" and [simp]: "S \<inter> T = T"
     using assms by auto
   have "?h2 C \<in> kernel ?G2 ?G1 ?h1" for C
   proof -
     have "?h1 (?h2 C)
        = (hom_induced (p-1) X {} X T id \<circ> hom_induced (p-1) (subtopology X S) {} X {} id \<circ> hom_boundary p X S) C"
       unfolding hom_relboundary_def
-      by (metis (no_types, lifting) comp_apply continuous_map_id continuous_map_id_subt empty_subsetI hom_induced_compose id_apply image_empty image_id order_refl)
+      by (metis Pi_empty comp_eq_dest_lhs continuous_map_id continuous_map_id_subt funcsetI hom_induced_compose' id_apply)
     also have "\<dots> = \<one>\<^bsub>?G1\<^esub>"
     proof -
       have *: "hom_boundary p X S C \<in> carrier ?H2"
@@ -2349,7 +2364,8 @@
       using that by (simp add: kernel_def)
     moreover
     have "hom_boundary (p-1) X T \<circ> hom_induced (p-1) (subtopology X S) T X T id = hom_boundary (p-1) (subtopology X S) T"
-      by (metis Int_lower2 \<open>S \<inter> T = T\<close> continuous_map_id_subt hom_relboundary_def hom_relboundary_empty id_apply image_id naturality_hom_induced subtopology_subtopology)
+      by (metis funcsetI  \<open>S \<inter> T = T\<close> continuous_map_id_subt hom_relboundary_def
+            hom_relboundary_empty id_apply naturality_hom_induced subtopology_subtopology)
     then have "hom_boundary (p-1) (subtopology X S) T x = \<one>\<^bsub>homology_group (p - 2) (subtopology (subtopology X S) T)\<^esub>"
       using naturality_hom_induced [of "subtopology X S" X id T T "p-1"] that
         hom_one [OF hom_boundary_hom group_relative_homology_group group_relative_homology_group, of "p-1" X T]
@@ -2416,14 +2432,14 @@
                     [hom_induced p X T X S id, hom_induced p (subtopology X S) T X T id])"
     (is "exact_seq ([?G1,?G2,?G3], [?h1,?h2])")
 proof -
-  have iTS: "id ` T \<subseteq> S" and [simp]: "S \<inter> T = T"
+  have iTS: "id \<in> T \<rightarrow> S" and [simp]: "S \<inter> T = T"
     using assms by auto
   have 1: "?h2 x \<in> kernel ?G2 ?G1 ?h1" for x
   proof -
     have "?h1 (?h2 x)
         = (hom_induced p (subtopology X S) S X S id \<circ>
            hom_induced p (subtopology X S) T (subtopology X S) S id) x"
-      by (metis comp_eq_dest_lhs continuous_map_id continuous_map_id_subt hom_induced_compose iTS id_apply image_subsetI)
+      by (simp add: hom_induced_compose' iTS)
     also have "\<dots> = \<one>\<^bsub>relative_homology_group p X S\<^esub>"
     proof -
       have "trivial_group (relative_homology_group p (subtopology X S) S)"
@@ -2451,7 +2467,8 @@
     have "hom_boundary p X S (hom_induced p X T X S id x)
         = hom_induced (p-1) (subtopology X T) {} (subtopology X S) {} id
             (hom_boundary p X T x)"
-      using naturality_hom_induced [of X X id T S p]  by (simp add: assms o_def) meson
+      using naturality_hom_induced [of X X id T S p] iTS
+      by (simp add: assms o_def) meson
     with bcarr have "hom_boundary p X T x \<in> hom_boundary p (subtopology X S) T ` carrier ?G3"
       using homology_exactness_axiom_2 [of p "subtopology X S" T] x
       apply (simp add: kernel_def set_eq_iff subtopology_subtopology)
@@ -2467,8 +2484,9 @@
     have yyy: "hom_boundary p X T y = \<one>\<^bsub>homology_group (p-1) (subtopology X T)\<^esub>"
       apply (simp add: y_def bcarr xcarr hom_induced_carrier hom_boundary_carrier hb.inv_solve_right')
       using naturality_hom_induced [of concl: p X T "subtopology X S" T id]
-      by (smt (verit, best) \<open>S \<inter> T = T\<close> bcarr comp_eq_dest continuous_map_id_subt hom_induced_id id_apply 
-          image_subset_iff subtopology_subtopology ueq)
+      by (metis \<open>S \<inter> T = T\<close> comp_eq_dest_lhs continuous_map_id_subt
+          hom_relboundary_def hom_relboundary_empty id_apply image_id
+          image_subset_iff_funcset subsetI subtopology_subtopology ueq)
     then have "y \<in> hom_induced p X {} X T id ` carrier (homology_group p X)"
       using homology_exactness_axiom_1 [of p X T] x ycarr by (auto simp: kernel_def)
     then obtain z where zcarr: "z \<in> carrier (homology_group p X)"
@@ -2478,7 +2496,7 @@
       by (meson group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced)
 
     have "hom_induced p X {} X S id z = (hom_induced p X T X S id \<circ> hom_induced p X {} X T id) z"
-      by (simp add: assms flip: hom_induced_compose)
+      using iTS by (simp add: assms flip: hom_induced_compose)
     also have "\<dots> = \<one>\<^bsub>relative_homology_group p X S\<^esub>"
       using x 1 by (simp add: kernel_def zeq y_def)
     finally have "hom_induced p X {} X S id z = \<one>\<^bsub>relative_homology_group p X S\<^esub>" .
diff -r 3529946fca19 -r b022c013b04b src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -9,8 +9,8 @@
 
 theorem Borsuk_odd_mapping_degree_step:
   assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
-    and f: "\<And>x. x \<in> topspace(nsphere n) \<Longrightarrow> (f \<circ> (\<lambda>x i. -x i)) x = ((\<lambda>x i. -x i) \<circ> f) x"
-    and fim: "f ` (topspace(nsphere(n - Suc 0))) \<subseteq> topspace(nsphere(n - Suc 0))"
+    and f: "\<And>u. u \<in> topspace(nsphere n) \<Longrightarrow> (f \<circ> (\<lambda>x i. -x i)) u = ((\<lambda>x i. -x i) \<circ> f) u"
+    and fim: "f \<in> (topspace(nsphere(n - Suc 0))) \<rightarrow> topspace(nsphere(n - Suc 0))"
   shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)"
 proof (cases "n = 0")
   case False
@@ -24,6 +24,8 @@
     by (force simp: neg_def)
   have equator_upper: "equator n \<subseteq> upper n"
     by (force simp: equator_def upper_def)
+  then have [simp]: "id \<in> equator n \<rightarrow> upper n"
+    by force
   have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n"
     by (simp add: usphere_def)
   let ?rhgn = "relative_homology_group n (nsphere n)"
@@ -41,12 +43,13 @@
   have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)"
     by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
   then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)"
-    "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
-    "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
-    using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
+                 "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
+                 "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
+    using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def 
+        subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
   have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f"
-    by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology)
-
+    by (metis cmf continuous_map_from_subtopology continuous_map_in_subtopology equ(1) 
+        fim subtopology_restrict topspace_subtopology)
   have "f x n = 0" if "x \<in> topspace (nsphere n)" "x n = 0" for x
   proof -
     have "x \<in> topspace (nsphere (n - Suc 0))"
@@ -56,7 +59,7 @@
     ultimately show ?thesis
       using fim by auto
   qed
-  then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
+  then have fimeq: "f \<in> (topspace (nsphere n) \<inter> equator n) \<rightarrow> topspace (nsphere n) \<inter> equator n"
     using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
   have "\<And>k. continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. - x k)"
     by (metis UNIV_I continuous_map_product_projection continuous_map_minus)
@@ -182,13 +185,13 @@
     show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id
         \<in> Group.iso (relative_homology_group n (lsphere n) (equator n))
             (?rhgn (upper n))"
-      apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def)
+      unfolding lsphere_def usphere_def equator_def lower_def upper_def
       using iso_relative_homology_group_lower_hemisphere by blast
     show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id
         \<in> Group.iso (relative_homology_group n (usphere n) (equator n))
             (?rhgn (lower n))"
-      apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def)
-      using iso_relative_homology_group_upper_hemisphere by blast+
+      unfolding lsphere_def usphere_def equator_def lower_def upper_def
+      using iso_relative_homology_group_upper_hemisphere by blast
     show "exact_seq
          ([?rhgn (lower n),
            ?rhgn (equator n),
@@ -383,7 +386,7 @@
       by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2)
     also have "\<dots> = hom_induced n (nsphere n) (topspace(nsphere n) \<inter> equator n) (nsphere n) (equator n) f
                      (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \<inter> equator n) id v)"
-      using fimeq by (simp add: hom_induced_compose' cmf)
+      using fimeq by (simp add: hom_induced_compose' cmf Pi_iff)
     also have "\<dots> = ?hi_ee f u"
       by (metis hom_induced inf.left_idem ueq)
     finally show ?thesis .
@@ -467,12 +470,13 @@
     let ?TE = "topspace (nsphere n) \<inter> equator n"
     have fneg: "(f \<circ> neg) x = (neg \<circ> f) x" if "x \<in> topspace (nsphere n)" for x
       using f [OF that] by (force simp: neg_def)
-    have neg_im: "neg ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
-      by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology)
+    have neg_im: "neg \<in> (topspace (nsphere n) \<inter> equator n) \<rightarrow> topspace (nsphere n) \<inter> equator n"
+      using cm_neg continuous_map_image_subset_topspace equator_def
+      by fastforce
     have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg
            = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
-      using neg_im fimeq cm_neg cmf
-      apply (simp add: flip: hom_induced_compose del: hom_induced_restrict)
+      using neg_im fimeq cm_neg cmf fneg
+      apply (simp flip: hom_induced_compose del: hom_induced_restrict)
       using fneg by (auto intro: hom_induced_eq)
     have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
         = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
@@ -577,18 +581,25 @@
       if "squashable t U" "squashable t V" for U V t
       unfolding homotopic_with_def
     proof (intro exI conjI allI ballI)
-      let ?h = "\<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
-      show "(\<lambda>x. ?h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
-        using that
+      define h where "h \<equiv> \<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
+      show "(\<lambda>x. h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
+        using that unfolding h_def
         by clarsimp (metis squashableD [OF \<open>squashable t V\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
-      have 1: "?h ` ({0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U)) \<subseteq> U"
-        by clarsimp (metis squashableD [OF \<open>squashable t U\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
-      show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
-                           (subtopology (Euclidean_space (Suc n)) U) ?h"
-        apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1)
-        apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV)
+      have "\<And>x y i. \<lbrakk>\<forall>k\<ge>Suc n. y k = 0; Suc n \<le> i\<rbrakk> \<Longrightarrow> ret ((1 - x) * t + x * y n) y i = 0"
+        by (simp add: ret_def)
+      then have "h \<in> {0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U) \<rightarrow> {x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U"
+        using  squashableD [OF \<open>squashable t U\<close>]  segment_bound_lemma
+        apply (clarsimp simp: h_def Pi_iff)
+        by (metis convex_bound_le eq_diff_eq ge_iff_diff_ge_0 linorder_le_cases)
+      moreover
+      have "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV)
+                           ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U))) (powertop_real UNIV) h"
+        apply (auto simp: h_def case_prod_unfold ret_def continuous_map_componentwise_UNIV)
          apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros)
         by (auto simp: cm_snd)
+      ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
+                           (subtopology (Euclidean_space (Suc n)) U) h"
+        by (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology)
     qed (auto simp: ret_def)
     have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)"
     proof -
@@ -624,7 +635,7 @@
       then have "ret 0 x \<in> topspace (Euclidean_space n)"
         if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
         using that by (metis continuous_map_image_subset_topspace image_subset_iff retraction_maps_def)
-      then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
+      then show "(ret 0) \<in> (lo \<inter> hi) \<rightarrow> topspace (Euclidean_space n) - S"
         by (auto simp: local.cong ret_def hi_def lo_def)
       show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
         using hw_sub [OF squashable squashable_0_lohi] by simp
@@ -1836,11 +1847,13 @@
 proof -
   have *: "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
     by (metis Euclidean_space_def \<open>n \<le> m\<close> inf.absorb_iff2 subset_Euclidean_space subtopology_subtopology topspace_Euclidean_space)
+  then have "openin (Euclidean_space m) (f ` U)"
+    by (metis "*" U assms(4) cmf continuous_map_in_subtopology invariance_of_domain_Euclidean_space)
   moreover have "U \<subseteq> topspace (subtopology (Euclidean_space m) U)"
     by (metis U inf.absorb_iff2 openin_subset openin_subtopology openin_topspace)
   ultimately show ?thesis
-    by (metis (no_types) U \<open>inj_on f U\<close> cmf continuous_map_in_subtopology inf.absorb_iff2
-        inf.orderE invariance_of_domain_Euclidean_space openin_imp_subset openin_subtopology openin_topspace)
+    by (metis "*" cmf continuous_map_image_subset_topspace dual_order.antisym
+        openin_imp_subset openin_topspace subset_openin_subtopology)
 qed
 
 corollary invariance_of_domain_Euclidean_space_embedding_map_gen:
@@ -2067,7 +2080,7 @@
 
 lemma homeomorphic_maps_iff_homeomorphism [simp]:
    "homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g"
-  unfolding homeomorphic_maps_def homeomorphism_def by force
+  by (force simp: Pi_iff homeomorphic_maps_def homeomorphism_def)
 
 lemma homeomorphic_space_iff_homeomorphic [simp]:
    "(top_of_set S) homeomorphic_space (top_of_set T) \<longleftrightarrow> S homeomorphic T"
@@ -2159,7 +2172,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes ope: "openin (top_of_set U) S"
       and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
-      and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+      and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
       and injf: "inj_on f S"
     shows "openin (top_of_set V) (f ` S)"
 proof -
@@ -2189,26 +2202,25 @@
       have "continuous_on ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<phi>'"
         if "continuous_on {x. \<forall>i\<ge>dim U. x i = 0} \<phi>'"
         using that by (force elim: continuous_on_subset)
-      moreover have "\<phi>' ` ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<subseteq> S"
+      moreover have "\<phi>' \<in> ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<rightarrow> S"
         if "\<forall>x\<in>U. \<phi>' (\<phi> x) = x"
         using that \<open>S \<subseteq> U\<close> by fastforce
       ultimately show "continuous_map (subtopology (Euclidean_space (dim U)) (\<phi> ` S)) (top_of_set S) \<phi>'"
         using hom unfolding homeomorphic_maps_def
-        by (simp add:  Euclidean_space_def subtopology_subtopology euclidean_product_topology)
+        by (simp add: Euclidean_space_def subtopology_subtopology euclidean_product_topology)
       show "continuous_map (top_of_set S) (top_of_set V) f"
         by (simp add: contf fim)
       show "continuous_map (top_of_set V) (Euclidean_space (dim V)) \<psi>"
         by (simp add: \<psi> homeomorphic_imp_continuous_map)
     qed
     show "inj_on (\<psi> \<circ> f \<circ> \<phi>') (\<phi> ` S)"
-      using injf hom
-      unfolding inj_on_def homeomorphic_maps_map
-      by simp (metis \<open>S \<subseteq> U\<close> \<psi>'\<psi> fim imageI subsetD)
+      using injf hom \<open>S \<subseteq> U\<close> \<psi>'\<psi> fim
+      by (simp add: inj_on_def homeomorphic_maps_map Pi_iff) (metis subsetD)
   qed
   ultimately have "openin (Euclidean_space (dim V)) (\<psi> ` f ` S)"
     by (simp add: image_comp)
-  then show ?thesis
-    by (simp add: fim homeomorphic_map_openness_eq [OF \<psi>])
+  with fim show ?thesis
+    by (auto simp: homeomorphic_map_openness_eq [OF \<psi>])
 qed
 
 lemma invariance_of_domain:
@@ -2279,7 +2291,7 @@
       by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
     show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
       by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
-    show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+    show "((+) (- b) \<circ> f \<circ> (+) a) \<in> (+) (- a) ` S \<rightarrow> (+) (- b) ` V"
       using fim by auto
     show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
       by (auto simp: inj_on_def) (meson inj_onD injf)
diff -r 3529946fca19 -r b022c013b04b src/HOL/Homology/Simplices.thy
--- a/src/HOL/Homology/Simplices.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Homology/Simplices.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -87,7 +87,7 @@
     unfolding g_def continuous_map_componentwise
     by (force intro: continuous_intros)
   moreover
-  have "g x y ` {0..1} \<subseteq> standard_simplex p" "g x y 0 = x" "g x y 1 = y"
+  have "g x y \<in> {0..1} \<rightarrow> standard_simplex p" "g x y 0 = x" "g x y 1 = y"
     if "x \<in> standard_simplex p" "y \<in> standard_simplex p" for x y
     using that by (auto simp: convex_standard_simplex g_def)
   ultimately
@@ -183,7 +183,7 @@
   shows "singular_simplex (p - Suc 0) X (singular_face p k f)"
 proof -
   let ?PT = "(powertop_real UNIV)"
-  have 0: "simplical_face k ` standard_simplex (p - Suc 0) \<subseteq> standard_simplex p"
+  have 0: "simplical_face k \<in> standard_simplex (p - Suc 0) \<rightarrow> standard_simplex p"
     using assms simplical_face_in_standard_simplex by auto
   have 1: "continuous_map (subtopology ?PT (standard_simplex (p - Suc 0)))
                           (subtopology ?PT (standard_simplex p))
@@ -341,8 +341,8 @@
 subsection\<open>Relative cycles $Z_pX (S)$ where $X$ is a topology and $S$ a subset \<close>
 
 definition singular_relcycle :: "nat \<Rightarrow> 'a topology \<Rightarrow> 'a set \<Rightarrow> ('a chain) \<Rightarrow> bool"
-  where "singular_relcycle p X S \<equiv>
-        \<lambda>c. singular_chain p X c \<and> (chain_boundary p c, 0) \<in> mod_subset (p-1) (subtopology X S)"
+  where "singular_relcycle \<equiv>
+        \<lambda>p X S c. singular_chain p X c \<and> (chain_boundary p c, 0) \<in> mod_subset (p-1) (subtopology X S)"
 
 abbreviation singular_relcycle_set
   where "singular_relcycle_set p X S \<equiv> Collect (singular_relcycle p X S)"
@@ -357,8 +357,8 @@
 qed
 
 lemma singular_relcycle:
-   "singular_relcycle p X S c \<longleftrightarrow>
-    singular_chain p X c \<and> singular_chain (p-1) (subtopology X S) (chain_boundary p c)"
+   "singular_relcycle \<equiv>
+    \<lambda>p X S c. singular_chain p X c \<and> singular_chain (p-1) (subtopology X S) (chain_boundary p c)"
   by (simp add: singular_relcycle_def mod_subset_def)
 
 lemma singular_relcycle_0 [simp]: "singular_relcycle p X S 0"
@@ -777,7 +777,7 @@
     \<Longrightarrow>  chain_map p f c = c"
   unfolding singular_chain_def
   by (erule frag_induction) (auto simp: chain_map_diff simplex_map_id_gen)
-
+                                                              
 lemma chain_map_ident:
    "singular_chain p X c \<Longrightarrow> chain_map p id c = c"
   by (simp add: chain_map_id_gen)
@@ -831,19 +831,20 @@
 qed auto
 
 lemma singular_relcycle_chain_map:
-  assumes "singular_relcycle p X S c" "continuous_map X X' g" "g ` S \<subseteq> T"
+  assumes "singular_relcycle p X S c" "continuous_map X X' g" "g \<in> S \<rightarrow> T"
   shows "singular_relcycle p X' T (chain_map p g c)"
 proof -
   have "continuous_map (subtopology X S) (subtopology X' T) g"
     using assms
-    using continuous_map_from_subtopology continuous_map_in_subtopology topspace_subtopology by fastforce
+    by (metis Pi_anti_mono continuous_map_from_subtopology continuous_map_in_subtopology 
+        openin_imp_subset openin_topspace subsetD)
   then show ?thesis
     using chain_boundary_chain_map [of p X c g]
     by (metis One_nat_def assms(1) assms(2) singular_chain_chain_map singular_relcycle)
 qed
 
 lemma singular_relboundary_chain_map:
-  assumes "singular_relboundary p X S c" "continuous_map X X' g" "g ` S \<subseteq> T"
+  assumes "singular_relboundary p X S c" "continuous_map X X' g" "g \<in> S \<rightarrow> T"
   shows "singular_relboundary p X' T (chain_map p g c)"
 proof -
   obtain d e where d: "singular_chain (Suc p) X d"
@@ -853,10 +854,11 @@
     using assms(2) d singular_chain_chain_map by blast
   moreover have "singular_chain p (subtopology X' T) (chain_map p g e)"
   proof -
-    have "\<forall>t. g ` topspace (subtopology t S) \<subseteq> T"
-      by (metis assms(3) closure_of_subset_subtopology closure_of_topspace dual_order.trans image_mono)
+    have "\<And>Y. g \<in> topspace (subtopology Y S) \<rightarrow> T"
+      using assms(3) by auto
     then show ?thesis
-      by (meson assms(2) continuous_map_from_subtopology continuous_map_in_subtopology e singular_chain_chain_map)
+      by (metis assms(2) continuous_map_from_subtopology continuous_map_into_subtopology e
+          singular_chain_chain_map) 
   qed
   moreover have "chain_boundary (Suc p) (chain_map (Suc p) g d) + chain_map p g e =
                  chain_map p g (chain_boundary (Suc p) d + e)"
@@ -1705,7 +1707,7 @@
 proof
   assume ?lhs
   then show ?rhs
-    by (simp add: simplicial_simplex_def singular_simplex_def continuous_map_in_subtopology set_mp)
+    by (simp add: simplicial_simplex)
 next
   assume R: ?rhs
   then have cm: "continuous_map
@@ -1777,7 +1779,7 @@
     have "(\<lambda>i. \<Sum>j\<le>p. m j i * x j) \<in> standard_simplex q"
       if "x \<in> standard_simplex p" for x
       using that m unfolding oriented_simplex_def singular_simplex_def
-      by (auto simp: continuous_map_in_subtopology image_subset_iff)
+      by (auto simp: continuous_map_in_subtopology Pi_iff)
     then show ?thesis
       unfolding oriented_simplex_def simplex_map_def
       apply (rule_tac x="\<lambda>j k. (\<Sum>i\<le>q. l i k * m j i)" in exI)
@@ -1785,7 +1787,7 @@
       done
   qed
   then show ?case
-    using f one
+    using f one 
     apply (simp add: simplicial_simplex_def)
     using singular_simplex_def singular_simplex_simplex_map by blast
 next
@@ -2492,7 +2494,7 @@
       and X: "topspace X \<subseteq> \<Union>\<C>"
       and p: "singular_chain p X c"
   obtains n where "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
-                      \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
+                      \<Longrightarrow> \<exists>V \<in> \<C>. f \<in> (standard_simplex p) \<rightarrow> V"
 proof (cases "c = 0")
   case False
   then show ?thesis
@@ -2511,7 +2513,7 @@
       case False
       have "\<exists>e. 0 < e \<and>
                 (\<forall>K. K \<subseteq> standard_simplex p \<longrightarrow> (\<forall>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<longrightarrow> \<bar>x i - y i\<bar> \<le> e)
-                     \<longrightarrow> (\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V))"
+                     \<longrightarrow> (\<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V))"
         if f: "f \<in> Poly_Mapping.keys c" for f
       proof -
         have ssf: "singular_simplex p X f"
@@ -2551,19 +2553,19 @@
              and Kd: "\<forall>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<longrightarrow> \<bar>x i - y i\<bar> \<le> d"
           then have "\<exists>U. U \<in> g ` \<C> \<and> K \<subseteq> U"
             using d [OF K] by auto
-          then show "\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+          then show "\<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
             using K geq by fastforce
         qed (rule \<open>d > 0\<close>)
       qed
       then obtain \<psi> where epos: "\<forall>f \<in> Poly_Mapping.keys c. 0 < \<psi> f"
                  and e: "\<And>f K. \<lbrakk>f \<in> Poly_Mapping.keys c; K \<subseteq> standard_simplex p;
                                 \<And>x y i. x \<in> K \<and> y \<in> K \<and> i \<le> p \<Longrightarrow> \<bar>x i - y i\<bar> \<le> \<psi> f\<rbrakk>
-                               \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+                               \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
         by metis
       obtain d where "0 < d"
                and d: "\<And>f K. \<lbrakk>f \<in> Poly_Mapping.keys c; K \<subseteq> standard_simplex p;
                               \<And>x y i. \<lbrakk>x \<in> K; y \<in> K; i \<le> p\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> d\<rbrakk>
-                              \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+                              \<Longrightarrow> \<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
       proof
         show "Inf (\<psi> ` Poly_Mapping.keys c) > 0"
           by (simp add: finite_less_Inf_iff \<open>c \<noteq> 0\<close> epos)
@@ -2572,7 +2574,7 @@
           and le: "\<And>x y i. \<lbrakk>x \<in> K; y \<in> K; i \<le> p\<rbrakk> \<Longrightarrow> \<bar>x i - y i\<bar> \<le> Inf (\<psi> ` Poly_Mapping.keys c)"
         then have lef: "Inf (\<psi> ` Poly_Mapping.keys c) \<le> \<psi> f"
           by (auto intro: cInf_le_finite)
-        show "\<exists>V. V \<in> \<C> \<and> f ` K \<subseteq> V"
+        show "\<exists>V. V \<in> \<C> \<and> f \<in> K \<rightarrow> V"
           using le lef by (blast intro: dual_order.trans e [OF fK])
       qed
       let ?d = "\<lambda>m. (simplicial_subdivision p ^^ m) (frag_of (restrict id (standard_simplex p)))"
@@ -2626,9 +2628,9 @@
         then have "\<bar>x i - y i\<bar> \<le> d"
           if "x \<in> g ` (standard_simplex p)" "y \<in> g ` (standard_simplex p)" "i \<le> p" for i x y
           using that by blast
-        ultimately show "\<exists>V\<in>\<C>. h ` standard_simplex p \<subseteq> V"
+        ultimately show "\<exists>V\<in>\<C>. h \<in> standard_simplex p \<rightarrow> V"
           using \<open>f \<in> Poly_Mapping.keys c\<close> d [of f "g ` standard_simplex p"]
-          by (simp add: Bex_def heq image_image)
+          using heq image_subset_iff_funcset by fastforce
       qed
     qed
   qed
@@ -2640,13 +2642,13 @@
       and X: "topspace X \<subseteq> \<Union>\<C>"
       and p: "singular_relcycle p X S c"
     obtains c' where "singular_relcycle p X S c'" "homologous_rel p X S c c'"
-                      "\<And>f. f \<in> Poly_Mapping.keys c' \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
+                      "\<And>f. f \<in> Poly_Mapping.keys c' \<Longrightarrow> \<exists>V \<in> \<C>. f \<in> (standard_simplex p) \<rightarrow> V"
 proof -
   have "singular_chain p X c"
        "(chain_boundary p c, 0) \<in> (mod_subset (p - Suc 0) (subtopology X S))"
     using p unfolding singular_relcycle_def by auto
   then obtain n where n: "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
-                            \<Longrightarrow> \<exists>V \<in> \<C>. f ` (standard_simplex p) \<subseteq> V"
+                            \<Longrightarrow> \<exists>V \<in> \<C>. f \<in> (standard_simplex p) \<rightarrow> V"
     by (blast intro: sufficient_iterated_singular_subdivision_exists [OF \<C> X])
   let ?c' = "(singular_subdivision p ^^ n) c"
   show ?thesis
@@ -2665,7 +2667,7 @@
   next
     fix f :: "(nat \<Rightarrow> real) \<Rightarrow> 'a"
     assume "f \<in> Poly_Mapping.keys ?c'"
-    then show "\<exists>V\<in>\<C>. f ` standard_simplex p \<subseteq> V"
+    then show "\<exists>V\<in>\<C>. f \<in> (standard_simplex p) \<rightarrow> V"
       by (rule n [OF order_refl])
   qed
 qed
@@ -2685,7 +2687,7 @@
        for p X c S and T U :: "'a set"
   proof -
     obtain n where n: "\<And>m f. \<lbrakk>n \<le> m; f \<in> Poly_Mapping.keys ((singular_subdivision p ^^ m) c)\<rbrakk>
-                             \<Longrightarrow> \<exists>V \<in> {S \<inter> X interior_of T, S - X closure_of U}. f ` standard_simplex p \<subseteq> V"
+                             \<Longrightarrow> \<exists>V \<in> {S \<inter> X interior_of T, S - X closure_of U}. f \<in> (standard_simplex p) \<rightarrow> V"
       apply (rule sufficient_iterated_singular_subdivision_exists
                    [of "{S \<inter> X interior_of T, S - X closure_of U}"])
       using X S c
@@ -2791,7 +2793,7 @@
 subsection\<open>Homotopy invariance\<close>
 
 theorem homotopic_imp_homologous_rel_chain_maps:
-  assumes hom: "homotopic_with (\<lambda>h. h ` T \<subseteq> V) S U f g" and c: "singular_relcycle p S T c"
+  assumes hom: "homotopic_with (\<lambda>h. h \<in> T \<rightarrow> V) S U f g" and c: "singular_relcycle p S T c"
   shows "homologous_rel p U V (chain_map p f c) (chain_map p g c)"
 proof -
   note sum.atMost_Suc [simp del]