proposition: Lemma morphpre_maximal : maximal (f @*^-1 M) (f @*^-1 G) = maximal M G.
proof: Proof. apply/maxgroupP/maxgroupP; rewrite morphpre_proper //= => [] [ltMG maxM]. split=> // H ltHG sMH; have dH := subset_trans (proper_sub ltHG) dG. rewrite -(morphpreK dH) [f @*^-1 H]maxM ?morphpreK ?morphpreSK //. by rewrite morphpre_proper. split=> // H ltHG sMH. have dH: H \subset D := subset_trans (proper_sub ltHG) (subsetIl D _). have defH: f @*^-1 (f @* H) = H. by apply: morphimGK dH; apply: subset_trans sMH; apply: ker_sub_pre. rewrite -defH morphpre_proper ?morphimS // in ltHG. by rewrite -defH [f @* H]maxM // -(morphpreK dM) morphimS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)