diff -r 733e256ecdf3 -r 6a9e2a82ea15 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Apr 03 12:55:27 2019 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Apr 03 14:55:30 2019 +0100
@@ -9,6 +9,11 @@
 imports Complete_Lattice "HOL-Library.FuncSet"
 begin
 
+(*MOVE*)
+lemma image_paired_Times:
+   "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
+  by auto
+
 section \<open>Monoids and Groups\<close>
 
 subsection \<open>Definitions\<close>
@@ -1250,10 +1255,6 @@
   using assms
   by (fastforce simp: hom_def Pi_def dest!: group.is_monoid)
 
-lemma image_paired_Times:
-   "(\<lambda>(x,y). (f x,g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
-  by auto
-
 lemma iso_paired2:
   assumes "group G" "group H"
   shows "(\<lambda>(x,y). (f x,g y)) \<in> iso (DirProd G H) (DirProd G' H') \<longleftrightarrow> f \<in> iso G G' \<and> g \<in> iso H H'"