proposition: Lemma morph_gact_irr A M : A \subset D1 -> M \subset R1 -> acts_irreducibly (f @* A) (h @* M) to2 = acts_irreducibly A M to1.
proof: Proof. move=> sAD1 sMR1. have [[injf defD2] [injh defR2]] := (isomP iso_f, isomP iso_h). have h_eq1 := morphim_injm_eq1 injh. apply/mingroupP/mingroupP=> [] [/andP[ntM actAM] minM]. split=> [|U]; first by rewrite -h_eq1 // ntM -(injmSK injf) ?morph_gastabs. case/andP=> ntU acts_fAU sUM; have sUR1 := subset_trans sUM sMR1. apply: (injm_morphim_inj injh) => //; apply: minM; last exact: morphimS. by rewrite h_eq1 // ntU -morph_gastabs ?morphimS. split=> [|U]; first by rewrite h_eq1 // ntM -morph_gastabs ?morphimS. case/andP=> ntU acts_fAU sUhM. have sUhR1 := subset_trans sUhM (morphimS h sMR1). have sU'M: h @*^-1 U \subset M by rewrite sub_morphpre_injm. rewrite /= -(minM _ _ sU'M) ?morphpreK // -h_eq1 ?subsetIl // -(injmSK injf) //. by rewrite morph_gastabs ?(subset_trans sU'M) // morphpreK ?ntU. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)