proposition: Lemma Sylow_setI_normal G H P : G <| H -> p.-Sylow(H) P -> p.-Sylow(G) (G :&: P).
proof: Proof. case/normalP=> sGH nGH sylP; have [Q sylQ] := Sylow_exists p G. have /maxgroupP[/andP[sQG pQ] maxQ] := Hall_max sylQ. have [R sylR sQR] := Sylow_superset (subset_trans sQG sGH) pQ. have [[x Hx ->] pR] := (Sylow_trans sylR sylP, pHall_pgroup sylR). rewrite -(nGH x Hx) -conjIg pHallJ2. have /maxQ-> //: Q \subset G :&: R by rewrite subsetI sQG. by rewrite /psubgroup subsetIl (pgroupS _ pR) ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)