proposition: Lemma asimpleI (N1 N2 : {group rT}) : N2 \subset 'N(N1) -> N1 \subset D -> [acts A, on N1 | to] -> [acts A, on N2 | to] -> asimple (to / N1) (N2 / N1) -> asimple (to / (N2 :&: N1)) (N2 / (N2 :&: N1)).
proof: Proof. move=> nN21 sN1D aN1 aN2 /asimpleP[ntQ1 max1]. have [f1 [f1e f1ker f1pre f1im]] := restrmP (coset_morphism N1) nN21. have hf2' : N2 \subset 'N(N2 :&: N1) by apply: normsI => //; rewrite normG. have hf2'' : 'ker (coset (N2 :&: N1)) \subset 'ker f1. by rewrite f1ker !ker_coset. pose f2 := factm_morphism hf2'' hf2'. apply/asimpleP; split. rewrite /= setIC; apply/negP; move: (second_isog nN21); move/isog_eq1->. by apply/negP. move=> H nHQ2 aH; pose K := f2 @* H. have nKQ1 : K <| N2 / N1. rewrite (_ : N2 / N1 = f2 @* (N2 / (N2 :&: N1))) ?morphim_normal //. by rewrite morphim_factm f1im. have sqA : qact_dom to N1 \subset A. by apply/subsetP=> t; rewrite qact_domE // inE; case/andP. have nNN2 : (N2 :&: N1) <| N2. by rewrite /normal subsetIl; apply: normsI => //; apply: normG. have aKQ1 : [acts qact_dom to N1, on K | to / N1]. pose H':= coset (N2 :&: N1)@*^-1 H. have eHH' : H :=: H' / (N2 :&: N1) by rewrite cosetpreK. have -> : K :=: f1 @* H' by rewrite /K eHH' morphim_factm. have sH'N2 : H' \subset N2. rewrite /H' eHH' quotientGK ?normal_cosetpre //=. by rewrite sub_cosetpre_quo ?normal_sub. have -> : f1 @* H' = coset N1 @* H' by rewrite f1im //=. apply: qacts_coset => //; apply: qacts_cosetpre => //; last exact: gactsI. by apply: (subset_trans (subsetIr _ _)). have injf2 : 'injm f2. by rewrite ker_factm f1ker /= ker_coset /= subG1 /= -quotientE trivg_quotient. have iHK : H \isog K. apply/isogP; pose f3 := restrm_morphism (normal_sub nHQ2) f2. by exists f3; rewrite 1?injm_restrm // morphim_restrm setIid. case: (max1 _ nKQ1 aKQ1). by move/eqP; rewrite -(isog_eq1 iHK); move/eqP->; left. move=> he /=; right; apply/eqP; rewrite eqEcard normal_sub //=. move: (second_isog nN21); rewrite setIC; move/card_isog->; rewrite -he. by move/card_isog: iHK=> <-; rewrite leqnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)