src/HOL/Homology/Homology_Groups.thy
changeset 78322 74c75da4cb01
parent 70095 e8f4ce87012b
child 78336 6bae28577994
--- a/src/HOL/Homology/Homology_Groups.thy	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/Homology/Homology_Groups.thy	Wed Jul 12 18:28:11 2023 +0100
@@ -508,8 +508,8 @@
         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]]
-      by (simp add: image_subset_iff subtopology_restrict continuous_map_def)
+      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>
                       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
@@ -530,10 +530,10 @@
         proof (cases "continuous_map X Y f")
           case True
           then have "f ` (topspace X \<inter> S) \<subseteq> topspace Y"
-            by (meson IntE continuous_map_def image_subsetI)
+            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]
+            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)
         qed (simp add: group.is_monoid)
       qed
@@ -543,7 +543,7 @@
               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
       using 2 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p c]
-      by simp (meson IntE continuous_map_def image_subsetI)
+            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>