proposition: Lemma morphimK A : A \subset D -> f @*^-1 (f @* A) = 'ker f * A.
proof: Proof. move=> sAD; apply/setP=> x; rewrite !inE. apply/idP/idP=> [/andP[Dx /morphimP[y Dy Ay eqxy]] | /imset2P[z y Kz Ay ->{x}]]. rewrite -(mulgKV y x) mem_mulg // !inE !(groupM, morphM, groupV) //. by rewrite morphV //= eqxy mulgV. have [Dy Dz]: y \in D /\ z \in D by rewrite (subsetP sAD) // dom_ker. by rewrite groupM // morphM // mker // mul1g imset_f // inE Dy. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)