proposition: Lemma isomP (f : {morphism G >-> rT}) : reflect ('injm f /\ f @* G = H) (isom G H f).
proof: Proof. apply: (iffP eqP) => [eqfGH | [injf <-]]; last first. by rewrite -injmD1 // morphimEsub ?subsetDl. split. apply/subsetP=> x /morphpreP[Gx fx1]; have: f x \notin H^# by rewrite inE fx1. by apply: contraR => ntx; rewrite -eqfGH imset_f // inE ntx. rewrite morphimEdom -{2}(setD1K (group1 G)) imsetU eqfGH. by rewrite imset_set1 morph1 setD1K. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)