proposition: Lemma Hall_pJsub p pi G H P : pi.-Hall(G) H -> p \in pi -> P \subset G -> p.-group P -> exists2 x, x \in G & P :^ x \subset H.
proof: Proof. move=> hallH pi_p sPG pP. have [S sylS] := Sylow_exists p H; have sylS_G := subHall_Sylow hallH pi_p sylS. have [x Gx sPxS] := Sylow_Jsub sylS_G sPG pP; exists x => //. exact: subset_trans sPxS (pHall_sub sylS). 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)