Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Weak_Morphisms.thy
changeset 69700 7a92cbec7030
parent 69122 1b5178abaf97 
--- a/src/HOL/Algebra/Weak_Morphisms.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Algebra/Weak_Morphisms.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -220,7 +220,8 @@
   have the_elem_hom: "(\<lambda>x. the_elem (f ` x)) \<in> hom (G Mod H) (image_group f G)"
     using weak_group_morphism_is_iso[OF assms] by (simp add: iso_def)
   have hom: "(\<lambda>x. the_elem (f ` x)) \<circ> (#>) H \<in> hom G (image_group f G)"
-    using hom_trans[OF H.r_coset_hom_Mod the_elem_hom] by simp
+    using hom_compose[OF H.r_coset_hom_Mod the_elem_hom]
+    using Group.hom_compose H.r_coset_hom_Mod the_elem_hom by blast
   have restrict: "\<And>a. a \<in> carrier G \<Longrightarrow> ((\<lambda>x. the_elem (f ` x)) \<circ> (#>) H) a = f a"
     using weak_group_morphism_range[OF assms] by auto
   show ?thesis
isabelle