proposition: Lemma isog_simple gT rT (G : {group gT}) (M : {group rT}) : G \isog M -> simple G = simple M.
proof: Proof. move=> eqGM; wlog suffices: gT rT G M eqGM / simple M -> simple G. by move=> IH; apply/idP/idP; apply: IH; rewrite // isog_sym. case/isogP: eqGM => f injf <- /simpleP[ntGf simGf]. apply/simpleP; split=> [|N nsNG]; first by rewrite -(morphim_injm_eq1 injf). rewrite -(morphim_invm injf (normal_sub nsNG)). have: f @* N <| f @* G by rewrite morphim_normal. by case/simGf=> /= ->; [left | right]; rewrite (morphim1, morphim_invm). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)