proposition: Lemma injm_char (G H : {group aT}) : G \subset D -> H \char G -> f @* H \char f @* G.
proof: Proof. move=> sGD /charP[sHG charH]. apply/charP; split=> [|g injg gfG]; first exact: morphimS. have /domP[h [_ ker_h _ im_h]]: 'dom (invm injf \o g \o f) = G. by rewrite /dom /= -(morphpreIim g) (setIidPl _) ?injmK // gfG morphimS. have hH: h @* H = H. apply: charH; first by rewrite ker_h !injm_comp ?injm_invm. by rewrite im_h !morphim_comp gfG morphim_invm. rewrite /= -{2}hH im_h !morphim_comp morphim_invmE morphpreK //. by rewrite (subset_trans _ (morphimS f sGD)) //= -{3}gfG !morphimS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)