src/HOL/Algebra/AbelCoset.thy

     fix x
     assume xcarr: "x \<in> carrier G"
     from a_subgroup have Hcarr: "H \<subseteq> carrier G"
       unfolding subgroup_def by simp
     from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
-      using m_comm [simplified] by fast
+      using m_comm [simplified] by fastforce
   qed
 qed
 
 lemma abelian_subgroupI3:
   fixes G (structure)