proposition: Theorem focal_subgroup_gen : S :&: G^`(1) = <<[set [~ x, u] | x in S, u in G & x ^ u \in S]>>.
proof: Proof. set K := <<_>>; set G' := G^`(1); have [sSG coSiSG] := andP (pHall_Hall sylS). apply/eqP; rewrite eqEsubset gen_subG andbC; apply/andP; split. apply/subsetP=> _ /imset2P[x u Sx /setIdP[Gu Sxu] ->]. by rewrite inE groupM ?groupV // mem_commg // (subsetP sSG). apply/subsetP=> g /setIP[Sg G'g]; have Gg := subsetP sSG g Sg. have nKS: S \subset 'N(K). rewrite norms_gen //; apply/subsetP=> y Sy; rewrite inE. apply/subsetP=> _ /imsetP[_ /imset2P[x u Sx /setIdP[Gu Sxu] ->] ->]. have Gy: y \in G := subsetP sSG y Sy. by rewrite conjRg imset2_f ?groupJ // inE -conjJg /= 2?groupJ. set alpha := restrm_morphism nKS (coset_morphism K). have alphim: (alpha @* S) = (S / K) by rewrite morphim_restrm setIid. have abelSK : abelian (alpha @* S). rewrite alphim sub_der1_abelian // genS //. apply/subsetP=> _ /imset2P[x y Sx Sy ->]. by rewrite imset2_f // inE (subsetP sSG) ?groupJ. set ker_trans := 'ker (transfer G abelSK). have G'ker : G' \subset ker_trans. rewrite gen_subG; apply/subsetP=> h; case/imset2P=> h1 h2 Gh1 Gh2 ->{h}. by rewrite !inE groupR // morphR //; apply/commgP; apply: addrC. have transg0: transfer G abelSK g = 0%R. by move/kerP: (subsetP G'ker g G'g); apply. have partX := rcosets_cycle_partition sSG Gg. have trX := transversalP partX; set X := transversal _ _ in trX. have /and3P[_ sXG _] := trX. have gGSeq0: (fmod abelSK (alpha g) *+ #|G : S| = 0)%R. rewrite -transg0 (transfer_cycle_expansion sSG abelSK Gg trX). rewrite -(sum_index_rcosets_cycle sSG Gg trX) -sumrMnr /restrm. apply: eq_bigr=> x Xx; rewrite -[(_ *+ _)%R]morphX ?mem_morphim //=. rewrite -morphX //= /restrm; congr fmod. apply/rcoset_kercosetP; rewrite /= -/K. - by rewrite (subsetP nKS) ?groupX. - rewrite (subsetP nKS) // conjgE invgK mulgA -mem_rcoset. exact: mulg_exp_card_rcosets. rewrite mem_rcoset -{1}[g ^+ _]invgK -conjVg -commgEl mem_gen ?imset2_f //. by rewrite groupV groupX. rewrite inE conjVg !groupV (subsetP sXG) //= conjgE invgK mulgA -mem_rcoset. exact: mulg_exp_card_rcosets. move: (congr_fmod gGSeq0). rewrite fmval0 morphX ?inE //= fmodK ?mem_morphim // /restrm /=. move/((congr1 (expgn^~ (expg_invn (S / K) #|G : S|))) _). rewrite expg1n expgK ?mem_quotient ?coprime_morphl // => Kg1. by rewrite coset_idr ?(subsetP nKS). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)