proposition: Theorem Sylow's_theorem : [/\ forall P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P, [transitive G, on 'Syl_p(G) | 'JG], forall P, p.-Sylow(G) P -> #|'Syl_p(G)| = #|G : 'N_G(P)| & prime p -> #|'Syl_p(G)| %% p = 1%N].
proof: Proof. pose maxp A P := [max P | p.-subgroup(A) P]; pose S := [set P | maxp G P]. pose oG := orbit 'JG%act G. have actS: [acts G, on S | 'JG]. apply/subsetP=> x Gx; rewrite 3!inE; apply/subsetP=> P; rewrite 3!inE. exact: max_pgroupJ. have S_pG P: P \in S -> P \subset G /\ p.-group P. by rewrite inE => /maxgroupp/andP[]. have SmaxN P Q: Q \in S -> Q \subset 'N(P) -> maxp 'N_G(P) Q. rewrite inE => /maxgroupP[/andP[sQG pQ] maxQ] nPQ. apply/maxgroupP; rewrite /psubgroup subsetI sQG nPQ. by split=> // R; rewrite subsetI -andbA andbCA => /andP[_]; apply: maxQ. have nrmG P: P \subset G -> P <| 'N_G(P). by move=> sPG; rewrite /normal subsetIr subsetI sPG normG. have sylS P: P \in S -> p.-Sylow('N_G(P)) P. move=> S_P; have [sPG pP] := S_pG P S_P. by rewrite normal_max_pgroup_Hall ?nrmG //; apply: SmaxN; rewrite ?normG. have{SmaxN} defCS P: P \in S -> 'Fix_(S |'JG)(P) = [set P]. move=> S_P; apply/setP=> Q; rewrite {1}in_setI {1}afixJG. apply/andP/set1P=> [[S_Q nQP]|->{Q}]; last by rewrite normG. apply/esym/val_inj; case: (S_pG Q) => //= sQG _. by apply: uniq_normal_Hall (SmaxN Q _ _ _) => //=; rewrite ?sylS ?nrmG. have{defCS} oG_mod: {in S &, forall P Q, #|oG P| = (Q \in oG P) %[mod p]}. move=> P Q S_P S_Q; have [sQG pQ] := S_pG _ S_Q. have soP_S: oG P \subset S by rewrite acts_sub_orbit. have /pgroup_fix_mod-> //: [acts Q, on oG P | 'JG]. apply/actsP=> x /(subsetP sQG) Gx R; apply: orbit_transl. exact: mem_orbit. rewrite -{1}(setIidPl soP_S) -setIA defCS // (cardsD1 Q) setDE. by rewrite -setIA setICr setI0 cards0 addn0 inE set11 andbT. have [P S_P]: exists P, P \in S. have: p.-subgroup(G) 1 by rewrite /psubgroup sub1G pgroup1. by case/(@maxgroup_exists _ (p.-subgroup(G))) => P; exists P; rewrite inE. have trS: [transitive G, on S | 'JG]. apply/imsetP; exists P => //; apply/eqP. rewrite eqEsubset andbC acts_sub_orbit // S_P; apply/subsetP=> Q S_Q. have /[1!inE] /maxgroupP[/andP[_ pP]] := S_P. have [-> max1 | ntP _] := eqVneq P 1%G. move/andP/max1: (S_pG _ S_Q) => Q1. by rewrite (group_inj (Q1 (sub1G Q))) orbit_refl. have:= oG_mod _ _ S_P S_P; rewrite (oG_mod _ Q) // orbit_refl. have p_gt1: p > 1 by apply: prime_gt1; case/pgroup_pdiv: pP. by case: (Q \in oG P) => //; rewrite mod0n modn_small. have oS1: prime p -> #|S| %% p = 1%N. move/prime_gt1 => p_gt1. by rewrite -(atransP trS P S_P) (oG_mod P P) // orbit_refl modn_small. have oSiN Q: Q \in S -> #|S| = #|G : 'N_G(Q)|. by move=> S_Q; rewrite -(atransP trS Q S_Q) card_orbit astab1JG. have sylP: p.-Sylow(G) P. rewrite pHallE; case: (S_pG P) => // -> /= pP. case p_pr: (prime p); last first. rewrite p_part lognE p_pr /= -trivg_card1; apply/idPn=> ntP. by case/pgroup_pdiv: pP p_pr => // ->. rewrite -(LagrangeI G 'N(P)) /= mulnC partnM ?cardG_gt0 // part_p'nat. by rewrite mul1n (card_Hall (sylS P S_P)). by rewrite p'natE // -indexgI -oSiN // /dvdn oS1. have eqS Q: maxp G Q = p.-Sylow(G) Q. apply/idP/idP=> [S_Q|]; last exact: Hall_max. have{} S_Q: Q \in S by rewrite inE. rewrite pHallE -(card_Hall sylP); case: (S_pG Q) => // -> _ /=. by case: (atransP2 trS S_P S_Q) => x _ ->; rewrite cardJg. have ->: 'Syl_p(G) = S by apply/setP=> Q; rewrite 2!inE. by split=> // Q sylQ; rewrite -oSiN ?inE ?eqS. 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)