Library MathComp.hall

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype finset.
Require Import prime fingroup morphism automorphism quotient action gproduct.
Require Import commutator center pgroup finmodule nilpotent sylow.
Require Import abelian maximal.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope.

Section Hall.

Implicit Type gT : finGroupType.

Theorem SchurZassenhaus_split gT (G H : {group gT}) :
  Hall G HH <| G[splits G, over H].
Proof.
move: {2}_.+1 (ltnSn #|G|) ⇒ n; elim: n ⇒ // n IHn in gT G H ×.
rewrite ltnSGn hallH nsHG; have [sHG nHG] := andP nsHG.
have [-> | [p pr_p pH]] := trivgVpdiv H.
  by apply/splitsP; G; rewrite inE -subG1 subsetIl mul1g eqxx.
have [P sylP] := Sylow_exists p H.
case nPG: (P <| G); last first.
  pose N := ('N_G(P))%G; have sNG: N \subset G by rewrite subsetIl.
  have eqHN_G: H × N = G by exact: Frattini_arg sylP.
  pose H' := (H :&: N)%G.
  have nsH'N: H' <| N.
    by rewrite /normal subsetIr normsI ?normG ?(subset_trans sNG).
  have eq_iH: #|G : H| = #|N| %/ #|H'|.
    rewrite -divgS // -(divnMl (cardG_gt0 H')) mulnC -eqHN_G.
    by rewrite -mul_cardG (mulnC #|H'|) divnMl // cardG_gt0.
  have hallH': Hall N H'.
    rewrite /Hall -divgS subsetIr //= -eq_iH.
    by case/andP: hallH_; apply: coprimeSg; exact: subsetIl.
  have: [splits N, over H'].
    apply: IHn hallH' nsH'N; apply: {n}leq_trans Gn.
    rewrite proper_card // properEneq sNG andbT; apply/eqPeqNG.
    by rewrite -eqNG normal_subnorm (subset_trans (pHall_sub sylP)) in nPG.
  case/splitsPK /complP[tiKN eqH'K].
  have sKN: K \subset N by rewrite -(mul1g K) -eqH'K mulSg ?sub1set.
  apply/splitsP; K; rewrite inE -subG1; apply/andP; split.
    by rewrite /= -(setIidPr sKN) setIA tiKN.
  by rewrite eqEsubset -eqHN_G mulgS // -eqH'K mulGS mulSg ?subsetIl.
pose Z := 'Z(P); pose Gbar := G / Z; pose Hbar := H / Z.
have sZP: Z \subset P by exact: center_sub.
have sZH: Z \subset H by exact: subset_trans (pHall_sub sylP).
have sZG: Z \subset G by exact: subset_trans sHG.
have nZG: Z <| G by apply: char_normal_trans nPG; exact: center_char.
have nZH: Z <| H by exact: normalS nZG.
have nHGbar: Hbar <| Gbar by exact: morphim_normal.
have hallHbar: Hall Gbar Hbar by apply: morphim_Hall (normal_norm _) _.
have: [splits Gbar, over Hbar].
  apply: IHn ⇒ //; apply: {n}leq_trans Gn; rewrite ltn_quotient //.
  apply/eqP⇒ /(trivg_center_pgroup (pHall_pgroup sylP))/eqP.
  rewrite trivg_card1 (card_Hall sylP) p_part -(expn0 p).
  by rewrite eqn_exp2l ?prime_gt1 // lognE pH pr_p cardG_gt0.
case/splitsPKbar /complP[tiHKbar eqHKbar].
have: Kbar \subset Gbar by rewrite -eqHKbar mulG_subr.
case/inv_quotientS⇒ //= ZK quoZK sZZK sZKG.
have nZZK: Z <| ZK by exact: normalS nZG.
have cardZK: #|ZK| = (#|Z| × #|G : H|)%N.
  rewrite -(Lagrange sZZK); congr (_ × _)%N.
  rewrite -card_quotient -?quoZK; last by case/andP: nZZK.
  rewrite -(divgS sHG) -(Lagrange sZG) -(Lagrange sZH) divnMl //.
  rewrite -!card_quotient ?normal_norm //= -/Gbar -/Hbar.
  by rewrite -eqHKbar (TI_cardMg tiHKbar) mulKn.
have: [splits ZK, over Z].
  rewrite (Gaschutz_split nZZK _ sZZK) ?center_abelian //; last first.
    rewrite -divgS // cardZK mulKn ?cardG_gt0 //.
    by case/andP: hallH_; exact: coprimeSg.
  by apply/splitsP; 1%G; rewrite inE -subG1 subsetIr mulg1 eqxx.
case/splitsPK /complP[tiZK eqZK].
have sKZK: K \subset ZK by rewrite -(mul1g K) -eqZK mulSg ?sub1G.
have tiHK: H :&: K = 1.
  apply/trivgP; rewrite /= -(setIidPr sKZK) setIA -tiZK setSI //.
  rewrite -quotient_sub1; last by rewrite subIset 1?normal_norm.
  by rewrite /= quotientGI //= -quoZK tiHKbar.
apply/splitsP; K; rewrite inE tiHK ?eqEcard subxx leqnn /=.
rewrite mul_subG ?(subset_trans sKZK) //= TI_cardMg //.
rewrite -(@mulKn #|K| #|Z|) ?cardG_gt0 // -TI_cardMg // eqZK.
by rewrite cardZK mulKn ?cardG_gt0 // Lagrange.
Qed.

Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
    solvable HK \subset 'N(H)K1 \subset H × K
    coprime #|H| #|K|#|K1| = #|K|
  exists2 x, x \in H & K1 :=: K :^ x.
Proof.
move: {2}_.+1 (ltnSn #|H|) ⇒ n; elim: n ⇒ // n IHn in gT H K K1 ×.
rewrite ltnSleHn solH nHK; have [-> | ] := eqsVneq H 1.
  rewrite mul1gsK1K _ eqK1K; 1; first exact: set11.
  by apply/eqP; rewrite conjsg1 eqEcard sK1K eqK1K /=.
pose G := (H <*> K)%G.
have defG: G :=: H × K by rewrite -normC // -norm_joinEl // joingC.
have sHG: H \subset G by exact: joing_subl.
have sKG: K \subset G by exact: joing_subr.
have nsHG: H <| G by rewrite /(H <| G) sHG join_subG normG.
case/(solvable_norm_abelem solH nsHG)=> M [sMH nsMG ntM] /and3P[_ abelM _].
have [sMG nMG] := andP nsMG; rewrite -defGsK1G coHK oK1K.
have nMsG (L : {set gT}): L \subset GL \subset 'N(M).
  by move/subset_trans→.
have [coKM coHMK]: coprime #|M| #|K| coprime #|H / M| #|K|.
  by apply/andP; rewrite -coprime_mull card_quotient ?nMsG ?Lagrange.
have oKM (K' : {group gT}): K' \subset G#|K'| = #|K|#|K' / M| = #|K|.
  movesK'G oK'.
  rewrite -quotientMidr -?norm_joinEl ?card_quotient ?nMsG //; last first.
    by rewrite gen_subG subUset sK'G.
  rewrite -divgS /=; last by rewrite -gen_subG genS ?subsetUr.
  by rewrite norm_joinEl ?nMsG // coprime_cardMg ?mulnK // oK' coprime_sym.
have [xb]: exists2 xb, xb \in H / M & K1 / M = (K / M) :^ xb.
  apply: IHn; try by rewrite (quotient_sol, morphim_norms, oKM K) ?(oKM K1).
    by apply: leq_trans leHn; rewrite ltn_quotient.
  by rewrite -morphimMl ?nMsG // -defG morphimS.
case/morphimPx nMx Hx ->{xb} eqK1Kx; pose K2 := (K :^ x)%G.
have{eqK1Kx} eqK12: K1 / M = K2 / M by rewrite quotientJ.
suff [y My ->]: exists2 y, y \in M & K1 :=: K2 :^ y.
  by (x × y); [rewrite groupMl // (subsetP sMH) | rewrite conjsgM].
have nMK1: K1 \subset 'N(M) by exact: nMsG.
have defMK: M × K1 = M <*> K1 by rewrite -normC // -norm_joinEl // joingC.
have sMKM: M \subset M <*> K1 by rewrite joing_subl.
have nMKM: M <| M <*> K1 by rewrite normalYl.
have trMK1: M :&: K1 = 1 by rewrite coprime_TIg ?oK1K.
have trMK2: M :&: K2 = 1 by rewrite coprime_TIg ?cardJg ?oK1K.
apply: (Gaschutz_transitive nMKM _ sMKM) ⇒ //=; last 2 first.
- by rewrite inE trMK1 defMK !eqxx.
- by rewrite -!(setIC M) trMK1.
- by rewrite -divgS //= -defMK coprime_cardMg oK1K // mulKn.
rewrite inE trMK2 eqxx eq_sym eqEcard /= -defMK andbC.
by rewrite !coprime_cardMg ?cardJg ?oK1K ?leqnn //= mulGS -quotientSK -?eqK12.
Qed.

Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) :
    solvable AA \subset 'N(G)B \subset A <*> G
    coprime #|G| #|A|#|A| = #|B|
  exists2 x, x \in G & B :=: A :^ x.
Proof.
set AG := A <*> G; move: {2}_.+1 (ltnSn #|AG|) ⇒ n.
elim: n ⇒ // n IHn in gT A B G AG ×.
rewrite ltnSleAn solA nGA sB_AG coGA oAB.
have [A1 | ntA] := eqsVneq A 1.
  by 1; rewrite // conjsg1 A1 (@card1_trivg _ B) // -oAB A1 cards1.
have [M [sMA nsMA ntM]] := solvable_norm_abelem solA (normal_refl A) ntA.
case/is_abelemPq q_pr /abelem_pgroup qM; have nMA := normal_norm nsMA.
have defAG: AG = A × G := norm_joinEl nGA.
have sA_AG: A \subset AG := joing_subl _ _.
have sG_AG: G \subset AG := joing_subr _ _.
have sM_AG := subset_trans sMA sA_AG.
have oAG: #|AG| = (#|A| × #|G|)%N by rewrite defAG coprime_cardMg 1?coprime_sym.
have q'G: #|G|`_q = 1%N.
  rewrite part_p'nat ?p'natE -?prime_coprime // coprime_sym.
  have [_ _ [k oM]] := pgroup_pdiv qM ntM.
  by rewrite -(@coprime_pexpr k.+1) // -oM (coprimegS sMA).
have coBG: coprime #|B| #|G| by rewrite -oAB coprime_sym.
have defBG: B × G = AG.
  by apply/eqP; rewrite eqEcard mul_subG ?sG_AG //= oAG oAB coprime_cardMg.
case nMG: (G \subset 'N(M)).
  have nsM_AG: M <| AG by rewrite /normal sM_AG join_subG nMA.
  have nMB: B \subset 'N(M) := subset_trans sB_AG (normal_norm nsM_AG).
  have sMB: M \subset B.
    have [Q sylQ]:= Sylow_exists q B; have sQB := pHall_sub sylQ.
    apply: subset_trans (normal_sub_max_pgroup (Hall_max _) qM nsM_AG) (sQB).
    rewrite pHallE (subset_trans sQB) //= oAG partnM // q'G muln1 oAB.
    by rewrite (card_Hall sylQ).
  have defAGq: AG / M = (A / M) <*> (G / M).
    by rewrite quotient_gen ?quotientU ?subUset ?nMA.
  have: B / M \subset (A / M) <*> (G / M) by rewrite -defAGq quotientS.
  case/IHn; rewrite ?morphim_sol ?quotient_norms ?coprime_morph //.
  - by rewrite -defAGq (leq_trans _ leAn) ?ltn_quotient.
  - by rewrite !card_quotient // -!divgS // oAB.
  moveMx; case/morphimPx Nx Gx ->{Mx} //; rewrite -quotientJ //= ⇒ defBq.
   x ⇒ //; apply: quotient_inj defBq; first by rewrite /normal sMB.
  by rewrite -(normsP nMG x Gx) /normal normJ !conjSg.
pose K := M <*> G; pose R := K :&: B; pose N := 'N_G(M).
have defK: K = M × G by rewrite -norm_joinEl ?(subset_trans sMA).
have oK: #|K| = (#|M| × #|G|)%N.
  by rewrite defK coprime_cardMg // coprime_sym (coprimegS sMA).
have sylM: q.-Sylow(K) M.
  by rewrite pHallE joing_subl /= oK partnM // q'G muln1 part_pnat_id.
have sylR: q.-Sylow(K) R.
  rewrite pHallE subsetIl /= -(card_Hall sylM) -(@eqn_pmul2r #|G|) // -oK.
  rewrite -coprime_cardMg ?(coprimeSg _ coBG) ?subsetIr //=.
  by rewrite group_modr ?joing_subr ?(setIidPl _) // defBG join_subG sM_AG.
have [mx] := Sylow_trans sylM sylR.
rewrite /= -/K defK; case/imset2Pm x Mm Gx ->{mx}.
rewrite conjsgM conjGid {m Mm}// ⇒ defR.
have sNG: N \subset G := subsetIl _ _.
have pNG: N \proper G by rewrite /proper sNG subsetI subxx nMG.
have nNA: A \subset 'N(N) by rewrite normsI ?norms_norm.
have: B :^ x^-1 \subset A <*> N.
  rewrite norm_joinEl ?group_modl // -defAG subsetI !sub_conjgV -normJ -defR.
  rewrite conjGid ?(subsetP sG_AG) // normsI ?normsG // (subset_trans sB_AG) //.
  by rewrite join_subG normsM // -defK normsG ?joing_subr.
do [case/IHn; rewrite ?cardJg ?(coprimeSg _ coGA) //= -/N] ⇒ [|y Ny defB].
  rewrite joingC norm_joinEr // coprime_cardMg ?(coprimeSg sNG) //.
  by rewrite (leq_trans _ leAn) // oAG mulnC ltn_pmul2l // proper_card.
(y × x); first by rewrite groupM // (subsetP sNG).
by rewrite conjsgM -defB conjsgKV.
Qed.

Lemma Hall_exists_subJ pi gT (G : {group gT}) :
  solvable Gexists2 H : {group gT}, pi.-Hall(G) H
                & K : {group gT}, K \subset Gpi.-group K
                  exists2 x, x \in G & K \subset H :^ x.
Proof.
move: {2}_.+1 (ltnSn #|G|) ⇒ n.
elim: n gT G ⇒ // n IHn gT G; rewrite ltnSleGn solG.
have [-> | ntG] := eqsVneq G 1.
   1%G ⇒ [|_ /trivGP_]; last by 1; rewrite ?set11 ?sub1G.
  by rewrite pHallE sub1G cards1 part_p'nat.
case: (solvable_norm_abelem solG (normal_refl _)) ⇒ // M [sMG nsMG ntM].
case/is_abelemPp pr_p /and3P[pM cMM _].
pose Gb := (G / M)%G; case: (IHn _ Gb) ⇒ [||Hb]; try exact: quotient_sol.
  by rewrite (leq_trans (ltn_quotient _ _)).
case/and3P⇒ [sHbGb piHb pi'Hb'] transHb.
case: (inv_quotientS nsMG sHbGb) ⇒ H def_H sMH sHG.
have nMG := normal_norm nsMG; have nMH := subset_trans sHG nMG.
have{transHb} transH (K : {group gT}):
  K \subset Gpi.-group Kexists2 x, x \in G & K \subset H :^ x.
- movesKG piK; have nMK := subset_trans sKG nMG.
  case: (transHb (K / M)%G) ⇒ [||xb Gxb sKHxb]; first exact: morphimS.
    exact: morphim_pgroup.
  case/morphimP: Gxbx Nx Gx /= def_x; x ⇒ //.
  apply/subsetPy Ky.
  have: y \in coset M y by rewrite val_coset (subsetP nMK, rcoset_refl).
  have: coset M y \in (H :^ x) / M.
    rewrite /quotient morphimJ //=.
    rewrite def_x def_H in sKHxb; apply: (subsetP sKHxb); exact: mem_quotient.
  case/morphimPz Nz Hxz →.
  rewrite val_coset //; case/rcosetPt Mt ->; rewrite groupMl //.
  by rewrite mem_conjg (subsetP sMH) // -mem_conjg (normP Nx).
have{pi'Hb'} pi'H': pi^'.-nat #|G : H|.
  move: pi'Hb'; rewrite -!divgS // def_H !card_quotient //.
  by rewrite -(divnMl (cardG_gt0 M)) !Lagrange.
have [pi_p | pi'p] := boolP (p \in pi).
   H ⇒ //; apply/and3P; split⇒ //; rewrite /pgroup.
  by rewrite -(Lagrange sMH) -card_quotient // pnat_mul -def_H (pi_pnat pM).
have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|.
  case: (IHn _ H (leq_trans ltHG leGn)) ⇒ [|H1]; first exact: solvableS solG.
  case/and3PsH1H piH1 pi'H1' transH1.
  have sH1G: H1 \subset G by exact: subset_trans sHG.
   H1 ⇒ [|K sKG piK].
    apply/and3P; split ⇒ //.
    rewrite -divgS // -(Lagrange sHG) -(Lagrange sH1H) -mulnA.
    by rewrite mulKn // pnat_mul pi'H1'.
  case: (transH K sKG piK) ⇒ x Gx def_K.
  case: (transH1 (K :^ x^-1)%G) ⇒ [||y Hy def_K1].
  - by rewrite sub_conjgV.
  - by rewrite /pgroup cardJg.
   (y × x); first by rewrite groupMr // (subsetP sHG).
  by rewrite -(conjsgKV x K) conjsgM conjSg.
have{leGH Gb sHbGb sHG sMH pi'H'} eqHG: H = G.
  by apply/eqP; rewrite -val_eqE eqEcard sHG.
have{H Hb def_H eqHG piHb nMH} hallM: pi^'.-Hall(G) M.
  rewrite /pHall /pgroup sMG pnatNK -card_quotient //=.
  by rewrite -eqHG -def_H (pi_pnat pM).
case/splitsP: (SchurZassenhaus_split (pHall_Hall hallM) nsMG) ⇒ H.
case/complPtrMH defG.
have sHG: H \subset G by rewrite -defG mulG_subr.
H ⇒ [|K sKG piK].
  apply: etrans hallM; rewrite /pHall sMG sHG /= -!divgS // -defG andbC.
  by rewrite (TI_cardMg trMH) mulKn ?mulnK // pnatNK.
pose G1 := (K <*> M)%G; pose K1 := (H :&: G1)%G.
have nMK: K \subset 'N(M) by apply: subset_trans sKG nMG.
have defG1: M × K = G1 by rewrite -normC -?norm_joinEl.
have sK1G1: K1 \subset M × K by rewrite defG1 subsetIr.
have coMK: coprime #|M| #|K|.
  by rewrite coprime_sym (pnat_coprime piK) //; exact: (pHall_pgroup hallM).
case: (SchurZassenhaus_trans_sol _ nMK sK1G1 coMK) ⇒ [||x Mx defK1].
- exact: solvableS solG.
- apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 M)) -TI_cardMg //; last first.
    by apply/trivgP; rewrite -trMH /= setIA subsetIl.
  rewrite -coprime_cardMg // defG1; apply/eqP; congr #|(_ : {set _})|.
  rewrite group_modl; last by rewrite -defG1 mulG_subl.
  by apply/setIidPr; rewrite defG gen_subG subUset sKG.
x^-1; first by rewrite groupV (subsetP sMG).
by rewrite -(_ : K1 :^ x^-1 = K) ?(conjSg, subsetIl) // defK1 conjsgK.
Qed.

End Hall.

Section HallCorollaries.

Variable gT : finGroupType.

Corollary Hall_exists pi (G : {group gT}) :
  solvable G H : {group gT}, pi.-Hall(G) H.
Proof. by case/(Hall_exists_subJ pi) ⇒ H; H. Qed.

Corollary Hall_trans pi (G H1 H2 : {group gT}) :
  solvable Gpi.-Hall(G) H1pi.-Hall(G) H2
  exists2 x, x \in G & H1 :=: H2 :^ x.
Proof.
movesolG; have [H hallH transH] := Hall_exists_subJ pi solG.
have conjH (K : {group gT}):
  pi.-Hall(G) Kexists2 x, x \in G & K = (H :^ x)%G.
- movehallK; have [sKG piK _] := and3P hallK.
  case: (transH K sKG piK) ⇒ x Gx sKH; x ⇒ //.
  apply/eqP; rewrite -val_eqE eqEcard sKH cardJg.
  by rewrite (card_Hall hallH) (card_Hall hallK) /=.
case/conjHx1 Gx1 ->{H1}; case/conjHx2 Gx2 ->{H2}.
(x2^-1 × x1); first by rewrite groupMl ?groupV.
by apply: val_inj; rewrite /= conjsgM conjsgK.
Qed.

Corollary Hall_superset pi (G K : {group gT}) :
  solvable GK \subset Gpi.-group K
    exists2 H : {group gT}, pi.-Hall(G) H & K \subset H.
Proof.
movesolG sKG; have [H hallH transH] := Hall_exists_subJ pi solG.
by case/transH⇒ // x Gx sKHx; (H :^ x)%G; rewrite ?pHallJ.
Qed.

Corollary Hall_subJ pi (G H K : {group gT}) :
    solvable Gpi.-Hall(G) HK \subset Gpi.-group K
  exists2 x, x \in G & K \subset H :^ x.
Proof.
movesolG HallH sKG piK; have [M HallM sKM]:= Hall_superset solG sKG piK.
have [x Gx defM] := Hall_trans solG HallM HallH.
by x; rewrite // -defM.
Qed.

Corollary Hall_Jsub pi (G H K : {group gT}) :
    solvable Gpi.-Hall(G) HK \subset Gpi.-group K
  exists2 x, x \in G & K :^ x \subset H.
Proof.
movesolG HallH sKG piK; have [x Gx sKHx] := Hall_subJ solG HallH sKG piK.
by x^-1; rewrite ?groupV // sub_conjgV.
Qed.

Lemma Hall_Frattini_arg pi (G K H : {group gT}) :
  solvable KK <| Gpi.-Hall(K) HK × 'N_G(H) = G.
Proof.
movesolK /andP[sKG nKG] hallH.
have sHG: H \subset G by apply: subset_trans sKG; case/andP: hallH.
rewrite setIC group_modl //; apply/setIidPr/subsetPx Gx.
pose H1 := (H :^ x^-1)%G.
have hallH1: pi.-Hall(K) H1 by rewrite pHallJnorm // groupV (subsetP nKG).
case: (Hall_trans solK hallH hallH1) ⇒ y Ky defH.
rewrite -(mulKVg y x) mem_mulg //; apply/normP.
by rewrite conjsgM {1}defH conjsgK conjsgKV.
Qed.

End HallCorollaries.

Section InternalAction.

Variables (pi : nat_pred) (gT : finGroupType).
Implicit Types G H K A X : {group gT}.

Lemma coprime_norm_cent A G :
  A \subset 'N(G)coprime #|G| #|A|'N_G(A) = 'C_G(A).
Proof.
movenGA coGA; apply/eqP; rewrite eqEsubset andbC setIS ?cent_sub //=.
rewrite subsetI subsetIl /= (sameP commG1P trivgP) -(coprime_TIg coGA).
rewrite subsetI commg_subr subsetIr andbT.
move: nGA; rewrite -commg_subl; apply: subset_trans.
by rewrite commSg ?subsetIl.
Qed.

Proposition coprime_Hall_exists A G :
    A \subset 'N(G)coprime #|G| #|A|solvable G
  exists2 H : {group gT}, pi.-Hall(G) H & A \subset 'N(H).
Proof.
movenGA coGA solG; have [H hallH] := Hall_exists pi solG.
have sG_AG: G \subset A <*> G by rewrite joing_subr.
have nG_AG: A <*> G \subset 'N(G) by rewrite join_subG nGA normG.
pose N := 'N_(A <*> G)(H)%G.
have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG.
have nGN_N: G :&: N <| N by rewrite /(_ <| N) subsetIr normsI ?normG.
have NG_AG: G × N = A <*> G.
  by apply: Hall_Frattini_arg hallH ⇒ //; exact/andP.
have iGN_A: #|N| %/ #|G :&: N| = #|A|.
  rewrite setIC divgI -card_quotient // -quotientMidl NG_AG.
  rewrite card_quotient -?divgS //= norm_joinEl //.
  by rewrite coprime_cardMg 1?coprime_sym // mulnK.
have hallGN: Hall N (G :&: N).
  by rewrite /Hall -divgS subsetIr //= iGN_A (coprimeSg _ coGA) ?subsetIl.
case/splitsP: {hallGN nGN_N}(SchurZassenhaus_split hallGN nGN_N) ⇒ B.
case/complPtrBGN defN.
have{trBGN iGN_A} oBA: #|B| = #|A|.
  by rewrite -iGN_A -{1}defN (TI_cardMg trBGN) mulKn.
have sBN: B \subset N by rewrite -defN mulG_subr.
case: (SchurZassenhaus_trans_sol solG nGA _ coGA oBA) ⇒ [|x Gx defB].
  by rewrite -(normC nGA) -norm_joinEl // -NG_AG -(mul1g B) mulgSS ?sub1G.
(H :^ x^-1)%G; first by rewrite pHallJ ?groupV.
apply/subsetPy Ay; have: y ^ x \in B by rewrite defB memJ_conjg.
move/(subsetP sBN)=> /setIP[_ /normP nHyx].
by apply/normP; rewrite -conjsgM conjgCV invgK conjsgM nHyx.
Qed.

Proposition coprime_Hall_trans A G H1 H2 :
    A \subset 'N(G)coprime #|G| #|A|solvable G
    pi.-Hall(G) H1A \subset 'N(H1)
    pi.-Hall(G) H2A \subset 'N(H2)
  exists2 x, x \in 'C_G(A) & H1 :=: H2 :^ x.
Proof.
move: H1H nGA coGA solG hallH nHA hallH2.
have{H2 hallH2} [x GxnH1xA] := Hall_trans solG hallH2 hallH.
have sG_AG: G \subset A <*> G by rewrite -{1}genGid genS ?subsetUr.
have nG_AG: A <*> G \subset 'N(G) by rewrite gen_subG subUset nGA normG.
pose N := 'N_(A <*> G)(H)%G.
have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG.
have nGN_N: G :&: N <| N.
  apply/normalP; rewrite subsetIr; split⇒ // y Ny.
  by rewrite conjIg (normP _) // (subsetP nGN, conjGid).
have NG_AG : G × N = A <*> G.
  by apply: Hall_Frattini_arg hallH ⇒ //; exact/andP.
have iGN_A: #|N : G :&: N| = #|A|.
  rewrite -card_quotient //; last by case/andP: nGN_N.
  rewrite (card_isog (second_isog nGN)) /= -quotientMidr (normC nGN) NG_AG.
  rewrite card_quotient // -divgS //= joingC norm_joinEr //.
  by rewrite coprime_cardMg // mulnC mulnK.
have solGN: solvable (G :&: N) by apply: solvableS solG; exact: subsetIl.
have oAxA: #|A :^ x^-1| = #|A| by exact: cardJg.
have sAN: A \subset N by rewrite subsetI -{1}genGid genS // subsetUl.
have nGNA: A \subset 'N(G :&: N).
  by apply/normsPy ?; rewrite conjIg (normsP nGA) ?(conjGid, subsetP sAN).
have coGNA: coprime #|G :&: N| #|A| := coprimeSg (subsetIl _ _) coGA.
case: (SchurZassenhaus_trans_sol solGN nGNA _ coGNA oAxA) ⇒ [|y GNy defAx].
  have ->: (G :&: N) × A = N.
    apply/eqP; rewrite eqEcard -{2}(mulGid N) mulgSS ?subsetIr //=.
    by rewrite coprime_cardMg // -iGN_A Lagrange ?subsetIr.
  rewrite sub_conjgV conjIg -normJ subsetI conjGid ?joing_subl //.
  by rewrite mem_gen // inE Gx orbT.
case/setIP: GNyGy; case/setIP_; move/normPnHy.
(y × x)^-1.
  rewrite -coprime_norm_cent // groupV inE groupM //=; apply/normP.
  by rewrite conjsgM -defAx conjsgKV.
by apply: val_inj; rewrite /= -{2}nHy -(conjsgM _ y) conjsgK.
Qed.

Lemma norm_conj_cent A G x : x \in 'C(A)
  (A \subset 'N(G :^ x)) = (A \subset 'N(G)).
Proof. by movecAx; rewrite norm_conj_norm ?(subsetP (cent_sub A)). Qed.

Lemma strongest_coprime_quotient_cent A G H :
      let R := H :&: [~: G, A] in
      A \subset 'N(H)R \subset Gcoprime #|R| #|A|
      solvable R || solvable A
  'C_G(A) / H = 'C_(G / H)(A / H).
Proof.
moveR nHA sRG coRA solRA.
have nRA: A \subset 'N(R) by rewrite normsI ?commg_normr.
apply/eqP; rewrite eqEsubset subsetI morphimS ?subsetIl //=.
rewrite (subset_trans _ (morphim_cent _ _)) ?morphimS ?subsetIr //=.
apply/subsetP_ /setIP[/morphimP[x Nx Gx ->] cAHx].
have{cAHx} cAxR y: y \in A[~ x, y] \in R.
  moveAy; have Ny: y \in 'N(H) by exact: subsetP Ay.
  rewrite inE mem_commg // andbT coset_idr ?groupR // morphR //=.
  by apply/eqP; apply/commgP; apply: (centP cAHx); rewrite mem_quotient.
have AxRA: A :^ x \subset R × A.
  apply/subsetP_ /imsetP[y Ay ->].
  rewrite -normC // -(mulKVg y (y ^ x)) -commgEl mem_mulg //.
  by rewrite -groupV invg_comm cAxR.
have [y Ry def_Ax]: exists2 y, y \in R & A :^ x = A :^ y.
  have oAx: #|A :^ x| = #|A| by rewrite cardJg.
  have [solR | solA] := orP solRA; first exact: SchurZassenhaus_trans_sol.
  by apply: SchurZassenhaus_trans_actsol; rewrite // joingC norm_joinEr.
rewrite -imset_coset; apply/imsetP; (x × y^-1); last first.
  by rewrite conjgCV mkerl // ker_coset memJ_norm groupV; case/setIP: Ry.
rewrite /= inE groupMl // ?(groupV, subsetP sRG) //=.
apply/centPz Az; apply/commgP/eqP/set1P.
rewrite -[[set 1]](coprime_TIg coRA) inE {1}commgEl commgEr /= -/R.
rewrite invMg -mulgA invgK groupMl // conjMg mulgA -commgEl.
rewrite groupMl ?cAxR // memJ_norm ?(groupV, subsetP nRA) // Ry /=.
by rewrite groupMr // conjVg groupV conjgM -mem_conjg -def_Ax memJ_conjg.
Qed.

Lemma coprime_norm_quotient_cent A G H :
    A \subset 'N(G)A \subset 'N(H)coprime #|H| #|A|solvable H
  'C_G(A) / H = 'C_(G / H)(A / H).
Proof.
movenGA nHA coHA solH; have sRH := subsetIl H [~: G, A].
rewrite strongest_coprime_quotient_cent ?(coprimeSg sRH) 1?(solvableS sRH) //.
by rewrite subIset // commg_subl nGA orbT.
Qed.

Lemma coprime_cent_mulG A G H :
     A \subset 'N(G)A \subset 'N(H)G \subset 'N(H)
     coprime #|H| #|A|solvable H
  'C_(H × G)(A) = 'C_H(A) × 'C_G(A).
Proof.
movenHA nGA nHG coHA solH; rewrite -norm_joinEr //.
have nsHG: H <| H <*> G by rewrite /normal joing_subl join_subG normG.
rewrite -{2}(setIidPr (normal_sub nsHG)) setIAC.
rewrite group_modr ?setSI ?joing_subr //=; symmetry; apply/setIidPl.
rewrite -quotientSK ?subIset 1?normal_norm //.
by rewrite !coprime_norm_quotient_cent ?normsY //= norm_joinEr ?quotientMidl.
Qed.

Lemma quotient_TI_subcent K G H :
    G \subset 'N(K)G \subset 'N(H)K :&: H = 1 →
  'C_K(G) / H = 'C_(K / H)(G / H).
Proof.
movenGK nGH tiKH.
have tiHR: H :&: [~: K, G] = 1.
  by apply/trivgP; rewrite /= setIC -tiKH setSI ?commg_subl.
apply: strongest_coprime_quotient_cent; rewrite ?tiHR ?sub1G ?solvable1 //.
by rewrite cards1 coprime1n.
Qed.

Proposition coprime_quotient_cent A G H :
    H \subset GA \subset 'N(H)coprime #|G| #|A|solvable G
  'C_G(A) / H = 'C_(G / H)(A / H).
Proof.
movesHG nHA coGA solG.
have sRG: H :&: [~: G, A] \subset G by rewrite subIset ?sHG.
by rewrite strongest_coprime_quotient_cent ?(coprimeSg sRG) 1?(solvableS sRG).
Qed.

Proposition coprime_comm_pcore A G K :
    A \subset 'N(G)coprime #|G| #|A|solvable G
    pi^'.-Hall(G) KK \subset 'C_G(A)
  [~: G, A] \subset 'O_pi(G).
Proof.
movenGA coGA solG hallK cKA.
case: (coprime_Hall_exists nGA) ⇒ // H hallH nHA.
have sHG: H \subset G by case/andP: hallH.
have sKG: K \subset G by case/andP: hallK.
have coKH: coprime #|K| #|H|.
  case/and3P: hallH_ piH _; case/and3P: hallK_ pi'K _.
  by rewrite coprime_sym (pnat_coprime piH pi'K).
have defG: G :=: K × H.
  apply/eqP; rewrite eq_sym eqEcard coprime_cardMg //.
  rewrite -{1}(mulGid G) mulgSS //= (card_Hall hallH) (card_Hall hallK).
  by rewrite mulnC partnC.
have sGA_H: [~: G, A] \subset H.
  rewrite gen_subG defG; apply/subsetPxya; case/imset2Pxy a.
  case/imset2Px y Kx HyAa → {xya xy}.
  rewrite commMgJ (([~ x, a] =P 1) _) ?(conj1g, mul1g).
    by rewrite groupMl ?groupV // memJ_norm ?(subsetP nHA).
  rewrite subsetI sKG in cKA; apply/commgP; exact: (centsP cKA).
apply: pcore_max; last first.
  by rewrite /(_ <| G) /= commg_norml commGC commg_subr nGA.
by case/and3P: hallH_ piH _; apply: pgroupS piH.
Qed.

End InternalAction.

Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) :
    A \subset 'N(G)coprime #|G| #|A|solvable G
    X \subset Gpi.-group XA \subset 'N(X)
   H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H].
Proof.
move: {2}_.+1 (ltnSn #|G|) ⇒ n.
elim: n ⇒ // n IHn in gT A G X × ⇒ leGn nGA coGA solG sXG piX nXA.
have [G1 | ntG] := eqsVneq G 1.
  case: (coprime_Hall_exists pi nGA) ⇒ // H hallH nHA.
  by H; split; rewrite // (subset_trans sXG) // G1 sub1G.
have sG_AG: G \subset A <*> G by rewrite joing_subr.
have sA_AG: A \subset A <*> G by rewrite joing_subl.
have nG_AG: A <*> G \subset 'N(G) by rewrite join_subG nGA normG.
have nsG_AG: G <| A <*> G by exact/andP.
case: (solvable_norm_abelem solG nsG_AG) ⇒ // M [sMG nsMAG ntM].
have{nsMAG} [nMA nMG]: A \subset 'N(M) G \subset 'N(M).
  by apply/andP; rewrite -join_subG normal_norm.
have nMX: X \subset 'N(M) by exact: subset_trans nMG.
case/is_abelemPp pr_p; case/and3PpM cMM _.
have: #|G / M| < n by rewrite (leq_trans (ltn_quotient _ _)).
move/(IHn _ (A / M)%G _ (X / M)%G); rewrite !(quotient_norms, quotientS) //.
rewrite !(coprime_morph, quotient_sol, morphim_pgroup) //.
case⇒ //= Hq []; case/and3PsHGq piHq pi'Hq' nHAq sXHq.
case/inv_quotientS: (sHGq) ⇒ [|HM defHM sMHM sHMG]; first exact/andP.
have nMHM := subset_trans sHMG nMG.
have{sXHq} sXHM: X \subset HM by rewrite -(quotientSGK nMX) -?defHM.
have{pi'Hq' sHGq} pi'HM': pi^'.-nat #|G : HM|.
  move: pi'Hq'; rewrite -!divgS // defHM !card_quotient //.
  by rewrite -(divnMl (cardG_gt0 M)) !Lagrange.
have{nHAq} nHMA: A \subset 'N(HM).
  by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; exact/andP.
case/orP: (orbN (p \in pi)) ⇒ pi_p.
   HM; split⇒ //; apply/and3P; split; rewrite /pgroup //.
  by rewrite -(Lagrange sMHM) pnat_mul -card_quotient // -defHM (pi_pnat pM).
case: (ltnP #|HM| #|G|) ⇒ [ltHG | leGHM {n IHn leGn}].
  case: (IHn _ A HM X (leq_trans ltHG leGn)) ⇒ // [||H [hallH nHA sXH]].
  - exact: coprimeSg coGA.
  - exact: solvableS solG.
  case/and3P: hallHsHHM piH pi'H'.
  have sHG: H \subset G by exact: subset_trans sHMG.
   H; split⇒ //; apply/and3P; split⇒ //.
  rewrite -divgS // -(Lagrange sHMG) -(Lagrange sHHM) -mulnA mulKn //.
  by rewrite pnat_mul pi'H'.
have{leGHM nHMA sHMG sMHM sXHM pi'HM'} eqHMG: HM = G.
  by apply/eqP; rewrite -val_eqE eqEcard sHMG.
have pi'M: pi^'.-group M by rewrite /pgroup (pi_pnat pM).
have{HM Hq nMHM defHM eqHMG piHq} hallM: pi^'.-Hall(G) M.
  apply/and3P; split; rewrite // /pgroup pnatNK.
  by rewrite -card_quotient // -eqHMG -defHM.
case: (coprime_Hall_exists pi nGA) ⇒ // H hallH nHA.
pose XM := (X <*> M)%G; pose Y := (H :&: XM)%G.
case/and3P: (hallH) ⇒ sHG piH _.
have sXXM: X \subset XM by rewrite joing_subl.
have co_pi_M (B : {group gT}): pi.-group Bcoprime #|B| #|M|.
  by movepiB; rewrite (pnat_coprime piB).
have hallX: pi.-Hall(XM) X.
  rewrite /pHall piX sXXM -divgS //= norm_joinEl //.
  by rewrite coprime_cardMg ?co_pi_M // mulKn.
have sXMG: XM \subset G by rewrite join_subG sXG.
have hallY: pi.-Hall(XM) Y.
  have sYXM: Y \subset XM by rewrite subsetIr.
  have piY: pi.-group Y by apply: pgroupS piH; exact: subsetIl.
  rewrite /pHall sYXM piY -divgS // -(_ : Y × M = XM).
    by rewrite coprime_cardMg ?co_pi_M // mulKn //.
  rewrite /= setIC group_modr ?joing_subr //=; apply/setIidPl.
  rewrite ((H × M =P G) _) // eqEcard mul_subG //= coprime_cardMg ?co_pi_M //.
  by rewrite (card_Hall hallM) (card_Hall hallH) partnC.
have nXMA: A \subset 'N(XM) by rewrite normsY.
have:= coprime_Hall_trans nXMA _ _ hallX nXA hallY.
rewrite !(coprimeSg sXMG, solvableS sXMG, normsI) //.
case⇒ // x /setIP[XMx cAx] →.
(H :^ x)%G; split; first by rewrite pHallJ ?(subsetP sXMG).
  by rewrite norm_conj_cent.
by rewrite conjSg subsetIl.
Qed.

Section ExternalAction.

Variables (pi : nat_pred) (aT gT : finGroupType).
Variables (A : {group aT}) (G : {group gT}) (to : groupAction A G).

Section FullExtension.

Local Notation inA := (sdpair2 to).
Local Notation inG := (sdpair1 to).
Local Notation A' := (inA @* gval A).
Local Notation G' := (inG @* gval G).
Let injG : 'injm inG := injm_sdpair1 _.
Let injA : 'injm inA := injm_sdpair2 _.

Hypotheses (coGA : coprime #|G| #|A|) (solG : solvable G).

Lemma external_action_im_coprime : coprime #|G'| #|A'|.
Proof. by rewrite !card_injm. Qed.

Let coGA' := external_action_im_coprime.

Let solG' : solvable G' := morphim_sol _ solG.

Let nGA' := im_sdpair_norm to.

Lemma ext_coprime_Hall_exists :
  exists2 H : {group gT}, pi.-Hall(G) H & [acts A, on H | to].
Proof.
have [H' hallH' nHA'] := coprime_Hall_exists pi nGA' coGA' solG'.
have sHG' := pHall_sub hallH'.
(inG @*^-1 H')%G ⇒ /=.
  by rewrite -(morphim_invmE injG) -{1}(im_invm injG) morphim_pHall.
by rewrite actsEsd ?morphpreK // subsetIl.
Qed.

Lemma ext_coprime_Hall_trans (H1 H2 : {group gT}) :
    pi.-Hall(G) H1[acts A, on H1 | to]
    pi.-Hall(G) H2[acts A, on H2 | to]
  exists2 x, x \in 'C_(G | to)(A) & H1 :=: H2 :^ x.
Proof.
movehallH1 nH1A hallH2 nH2A.
have sH1G := pHall_sub hallH1; have sH2G := pHall_sub hallH2.
rewrite !actsEsd // in nH1A nH2A.
have hallH1': pi.-Hall(G') (inG @* H1) by rewrite morphim_pHall.
have hallH2': pi.-Hall(G') (inG @* H2) by rewrite morphim_pHall.
have [x'] := coprime_Hall_trans nGA' coGA' solG' hallH1' nH1A hallH2' nH2A.
case/setIP⇒ /= Gx' cAx' /eqP defH1; pose x := invm injG x'.
have Gx: x \in G by rewrite -(im_invm injG) mem_morphim.
have def_x': x' = inG x by rewrite invmK.
x; first by rewrite inE Gx gacentEsd mem_morphpre /= -?def_x'.
apply/eqP; move: defH1; rewrite def_x' /= -morphimJ //=.
by rewrite !eqEsubset !injmSK // conj_subG.
Qed.

Lemma ext_norm_conj_cent (H : {group gT}) x :
    H \subset Gx \in 'C_(G | to)(A)
  [acts A, on H :^ x | to] = [acts A, on H | to].
Proof.
movesHG /setIP[Gx].
rewrite gacentEsd !actsEsd ?conj_subG ?morphimJ // 2!inE Gx /=.
exact: norm_conj_cent.
Qed.

Lemma ext_coprime_Hall_subset (X : {group gT}) :
    X \subset Gpi.-group X[acts A, on X | to]
   H : {group gT},
    [/\ pi.-Hall(G) H, [acts A, on H | to] & X \subset H].
Proof.
movesXG piX; rewrite actsEsd // ⇒ nXA'.
case: (coprime_Hall_subset nGA' coGA' solG' _ (morphim_pgroup _ piX) nXA').
  exact: morphimS.
moveH' /= [piH' nHA' sXH']; have sHG' := pHall_sub piH'.
(inG @*^-1 H')%G; rewrite actsEsd ?subsetIl ?morphpreK // nHA'.
rewrite -sub_morphim_pre //= sXH'; split⇒ //.
by rewrite -(morphim_invmE injG) -{1}(im_invm injG) morphim_pHall.
Qed.

End FullExtension.

Lemma ext_coprime_quotient_cent (H : {group gT}) :
    H \subset G[acts A, on H | to]coprime #|H| #|A|solvable H
 'C_(|to)(A) / H = 'C_(|to / H)(A).
Proof.
movesHG nHA coHA solH; pose N := 'N_G(H).
have nsHN: H <| N by rewrite normal_subnorm.
have [sHN nHn] := andP nsHN.
have sNG: N \subset G by exact: subsetIl.
have nNA: {acts A, on group N | to}.
  split; rewrite // actsEsd // injm_subnorm ?injm_sdpair1 //=.
  by rewrite normsI ?norms_norm ?im_sdpair_norm -?actsEsd.
rewrite -!(gacentIdom _ A) -quotientInorm -gacentIim setIAC.
rewrite -(gacent_actby nNA) gacentEsd -morphpreIim /= -/N.
have:= (injm_sdpair1 <[nNA]>, injm_sdpair2 <[nNA]>).
set inG := sdpair1 _; set inA := sdpair2 _ ⇒ [[injG injA]].
set G' := inG @* N; set A' := inA @* A; pose H' := inG @* H.
have defN: 'N(H | to) = A by apply/eqP; rewrite eqEsubset subsetIl.
have def_Dq: qact_dom to H = A by rewrite qact_domE.
have sAq: A \subset qact_dom to H by rewrite def_Dq.
rewrite {2}def_Dq -(gacent_ract _ sAq); set to_q := (_ \ _)%gact.
have:= And3 (sdprod_sdpair to_q) (injm_sdpair1 to_q) (injm_sdpair2 to_q).
rewrite gacentEsd; set inAq := sdpair2 _; set inGq := sdpair1 _ ⇒ /=.
set Gq := inGq @* _; set Aq := inAq @* _ ⇒ [[q_d iGq iAq]].
have nH': 'N(H') = setT.
  apply/eqP; rewrite -subTset -im_sdpair mulG_subG morphim_norms //=.
  by rewrite -actsEsd // acts_actby subxx /= (setIidPr sHN).
have: 'dom (coset H' \o inA \o invm iAq) = Aq.
  by rewrite ['dom _]morphpre_invm /= nH' morphpreT.
case/domPqA [def_qA ker_qA _ im_qA].
have{coHA} coHA': coprime #|H'| #|A'| by rewrite !card_injm.
have{ker_qA} injAq: 'injm qA.
  rewrite {}ker_qA !ker_comp ker_coset morphpre_invm -morphpreIim /= setIC.
  by rewrite coprime_TIg // -kerE (trivgP injA) morphim1.
have{im_qA} im_Aq : qA @* Aq = A' / H'.
  by rewrite {}im_qA !morphim_comp im_invm.
have: 'dom (quotm (sdpair1_morphism <[nNA]>) nsHN \o invm iGq) = Gq.
  by rewrite ['dom _]morphpre_invm /= quotientInorm.
case/domPqG [def_qG ker_qG _ im_qG].
have{ker_qG} injGq: 'injm qG.
  rewrite {}ker_qG ker_comp ker_quotm morphpre_invm (trivgP injG).
  by rewrite quotient1 morphim1.
have im_Gq: qG @* Gq = G' / H'.
  rewrite {}im_qG morphim_comp im_invm morphim_quotm //= -/inG -/H'.
  by rewrite -morphimIdom setIAC setIid.
have{def_qA def_qG} q_J : {in Gq & Aq, morph_act 'J 'J qG qA}.
  movex' a'; case/morphimPHx; case/morphimPx nHx GxGHx ->{Hx x'}.
  case/morphimPa _ Aa ->{a'} /=; rewrite -/inAq -/inGq.
  rewrite !{}def_qG {}def_qA /= !invmE // -sdpair_act //= -/inG -/inA.
  have Nx: x \in N by rewrite inE Gx.
  have Nxa: to x a \in N by case: (nNA); move/acts_act→.
  have [Gxa nHxa] := setIP Nxa.
  rewrite invmE qactE ?quotmE ?mem_morphim ?def_Dq //=.
  by rewrite -morphJ /= ?nH' ?inE // -sdpair_act //= actbyE.
pose q := sdprodm q_d q_J.
have{injAq injGq} injq: 'injm q.
  rewrite injm_sdprodm injAq injGq /= {}im_Aq {}im_Gq -/Aq .
  by rewrite -quotientGI ?im_sdpair_TI ?morphimS //= quotient1.
rewrite -[inGq @*^-1 _]morphpreIim -/Gq.
have sC'G: inG @*^-1 'C_G'(A') \subset G by rewrite !subIset ?subxx.
rewrite -[_ / _](injmK iGq) ?quotientS //= -/inGq; congr (_ @*^-1 _).
apply: (injm_morphim_inj injq); rewrite 1?injm_subcent ?subsetT //= -/q.
rewrite 2?morphim_sdprodml ?morphimS //= im_Gq.
rewrite morphim_sdprodmr ?morphimS //= im_Aq.
rewrite {}im_qG morphim_comp morphim_invm ?morphimS //.
rewrite morphim_quotm morphpreK ?subsetIl //= -/H'.
rewrite coprime_norm_quotient_cent ?im_sdpair_norm ?nH' ?subsetT //=.
exact: morphim_sol.
Qed.

End ExternalAction.

Section SylowSolvableAct.

Variables (gT : finGroupType) (p : nat).
Implicit Types A B G X : {group gT}.

Lemma sol_coprime_Sylow_exists A G :
    solvable AA \subset 'N(G)coprime #|G| #|A|
  exists2 P : {group gT}, p.-Sylow(G) P & A \subset 'N(P).
Proof.
movesolA nGA coGA; pose AG := A <*> G.
have nsG_AG: G <| AG by rewrite /normal joing_subr join_subG nGA normG.
have [sG_AG nG_AG]:= andP nsG_AG.
have [P sylP] := Sylow_exists p G; pose N := 'N_AG(P); pose NG := G :&: N.
have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG.
have sNG_G: NG \subset G := subsetIl G N.
have nsNG_N: NG <| N by rewrite /normal subsetIr normsI ?normG.
have defAG: G × N = AG := Frattini_arg nsG_AG sylP.
have oA : #|A| = #|N| %/ #|NG|.
  rewrite /NG setIC divgI -card_quotient // -quotientMidl defAG.
  rewrite card_quotient -?divgS //= norm_joinEl //.
  by rewrite coprime_cardMg 1?coprime_sym // mulnK.
have: [splits N, over NG].
  rewrite SchurZassenhaus_split // /Hall -divgS subsetIr //.
  by rewrite -oA (coprimeSg sNG_G).
case/splitsPB; case/complPtNG_B defN.
have [nPB]: B \subset 'N(P) B \subset AG.
  by apply/andP; rewrite andbC -subsetI -/N -defN mulG_subr.
case/SchurZassenhaus_trans_actsol ⇒ // [|x Gx defB].
  by rewrite oA -defN TI_cardMg // mulKn.
(P :^ x^-1)%G; first by rewrite pHallJ ?groupV.
by rewrite normJ -sub_conjg -defB.
Qed.

Lemma sol_coprime_Sylow_trans A G :
    solvable AA \subset 'N(G)coprime #|G| #|A|
  [transitive 'C_G(A), on [set P in 'Syl_p(G) | A \subset 'N(P)] | 'JG].
Proof.
movesolA nGA coGA; pose AG := A <*> G; set FpA := finset _.
have nG_AG: AG \subset 'N(G) by rewrite join_subG nGA normG.
have [P sylP nPA] := sol_coprime_Sylow_exists solA nGA coGA.
pose N := 'N_AG(P); have sAN: A \subset N by rewrite subsetI joing_subl.
have trNPA: A :^: AG ::&: N = A :^: N.
  pose NG := 'N_G(P); have sNG_G : NG \subset G := subsetIl _ _.
  have nNGA: A \subset 'N(NG) by rewrite normsI ?norms_norm.
  apply/setPAx; apply/setIdP/imsetP⇒ [[]|[x Nx ->{Ax}]]; last first.
    by rewrite conj_subG //; case/setIP: NxAGx; rewrite mem_imset.
  have ->: N = A <*> NG by rewrite /N /AG !norm_joinEl // -group_modl.
  have coNG_A := coprimeSg sNG_G coGA; case/imsetPx AGx ->{Ax}.
  case/SchurZassenhaus_trans_actsol; rewrite ?cardJg // ⇒ y Ny /= →.
  by y; rewrite // mem_gen 1?inE ?Ny ?orbT.
have{trNPA}: [transitive 'N_AG(A), on FpA | 'JG].
  have ->: FpA = 'Fix_('Syl_p(G) | 'JG)(A).
    by apply/setPQ; rewrite 4!inE afixJG.
  have SylP : P \in 'Syl_p(G) by rewrite inE.
  apply/(trans_subnorm_fixP _ SylP); rewrite ?astab1JG //.
  rewrite (atrans_supgroup _ (Syl_trans _ _)) ?joing_subr //= -/AG.
  by apply/actsPx /= AGx Q /=; rewrite !inE -{1}(normsP nG_AG x) ?pHallJ2.
rewrite {1}/AG norm_joinEl // -group_modl ?normG ?coprime_norm_cent //=.
rewrite -cent_joinEr ?subsetIr // ⇒ trC_FpA.
have FpA_P: P \in FpA by rewrite !inE sylP.
apply/(subgroup_transitiveP FpA_P _ trC_FpA); rewrite ?joing_subr //=.
rewrite astab1JG cent_joinEr ?subsetIr // -group_modl // -mulgA.
by congr (_ × _); rewrite mulSGid ?subsetIl.
Qed.

Lemma sol_coprime_Sylow_subset A G X :
  A \subset 'N(G)coprime #|G| #|A|solvable A
  X \subset Gp.-group XA \subset 'N(X)
   P : {group gT}, [/\ p.-Sylow(G) P, A \subset 'N(P) & X \subset P].
Proof.
movenGA coGA solA sXG pX nXA.
pose nAp (Q : {group gT}) := [&& p.-group Q, Q \subset G & A \subset 'N(Q)].
have: nAp X by exact/and3P.
case/maxgroup_existsR; case/maxgroupP; case/and3PpR sRG nRA maxR sXR.
have [P sylP sRP]:= Sylow_superset sRG pR.
suffices defP: P :=: R by P; rewrite sylP defP.
case/and3P: sylPsPG pP _; apply: (nilpotent_sub_norm (pgroup_nil pP)) ⇒ //.
pose N := 'N_G(R); have{sPG} sPN_N: 'N_P(R) \subset N by exact: setSI.
apply: norm_sub_max_pgroup (pgroupS (subsetIl _ _) pP) sPN_N (subsetIr _ _).
have nNA: A \subset 'N(N) by rewrite normsI ?norms_norm.
have coNA: coprime #|N| #|A| by apply: coprimeSg coGA; rewrite subsetIl.
have{solA coNA} [Q sylQ nQA] := sol_coprime_Sylow_exists solA nNA coNA.
suffices defQ: Q :=: R by rewrite max_pgroup_Sylow -{2}defQ.
apply: maxR; first by apply/and3P; case/and3P: sylQ; rewrite subsetI; case/andP.
by apply: normal_sub_max_pgroup (Hall_max sylQ) pR _; rewrite normal_subnorm.
Qed.

End SylowSolvableAct.