proposition: Theorem Baer_Suzuki x G : x \in G -> (forall y, y \in G -> p.-group <<[set x; x ^ y]>>) -> x \in 'O_p(G).
proof: Proof. have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE. set E := x ^: G; have{} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->]. rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ. by rewrite pE // groupMl ?groupV. have sEG: <<E>> \subset G by rewrite gen_subG class_subG. have nEG: G \subset 'N(E) by apply: class_norm. have Ex: x \in E by apply: class_refl. have [P Px sylP]: exists2 P : {group gT}, x \in P & p.-Sylow(<<E>>) P. have sxxE: <<[set x; x]>> \subset <<E>> by rewrite genS // setUid sub1set. have{sxxE} [P sylP sxxP] := Sylow_superset sxxE (pE _ _ Ex Ex). by exists P => //; rewrite (subsetP sxxP) ?mem_gen ?setU11. case sEP: (E \subset P). apply: subsetP Ex; rewrite -gen_subG; apply: pcore_max. by apply: pgroupS (pHall_pgroup sylP); rewrite gen_subG. by rewrite /normal gen_subG class_subG // norms_gen. pose P_yD D := [pred y in E :\: P | p.-group <<y |: D>>]. pose P_D := [pred D : {set gT} | D \subset P :&: E & [exists y, P_yD D y]]. have{Ex Px}: P_D [set x]. rewrite /= sub1set inE Px Ex; apply/existsP=> /=. by case/subsetPn: sEP => y Ey Py; exists y; rewrite inE Ey Py pE. case/(@maxset_exists _ P_D)=> D /maxsetP[]; rewrite {P_yD P_D}/=. rewrite subsetI sub1set -andbA => /and3P[sDP sDE /existsP[y0]]. set B := _ |: D; rewrite inE -andbA => /and3P[Py0 Ey0 pB] maxD Dx. have sDgE: D \subset <<E>> by apply: sub_gen. have sDG: D \subset G by apply: subset_trans sEG. have sBE: B \subset E by rewrite subUset sub1set Ey0. have sBG: <<B>> \subset G by apply: subset_trans (genS _) sEG. have sDB: D \subset B by rewrite subsetUr. have defD: D :=: P :&: <<B>> :&: E. apply/eqP; rewrite eqEsubset ?subsetI sDP sDE sub_gen //=. apply/setUidPl; apply: maxD; last apply: subsetUl. rewrite subUset subsetI sDP sDE setIAC subsetIl. apply/existsP; exists y0; rewrite inE Py0 Ey0 /= setUA -/B. by rewrite -[<<_>>]joing_idl joingE setKI genGid. have nDD: D \subset 'N(D). apply/subsetP=> z Dz; rewrite inE defD. apply/subsetP=> _ /imsetP[y /setIP[PBy Ey] ->]. rewrite inE groupJ // ?inE ?(subsetP sDP) ?mem_gen ?setU1r //= memJ_norm //. exact: (subsetP (subset_trans sDG nEG)). case nDG: (G \subset 'N(D)). apply: subsetP Dx; rewrite -gen_subG pcore_max ?(pgroupS (genS _) pB) //. by rewrite /normal gen_subG sDG norms_gen. have{n leGn IHn nDG} pN: p.-group <<'N_E(D)>>. apply: pgroupS (pcore_pgroup p 'N_G(D)); rewrite gen_subG /=. apply/subsetP=> x1 /setIP[Ex1 Nx1]; apply: IHn => [||y Ny]. - apply: leq_trans leGn; rewrite proper_card // /proper subsetIl. by rewrite subsetI nDG andbF. - by rewrite inE Nx1 (subsetP sEG) ?mem_gen. have Ex1y: x1 ^ y \in E. by rewrite -mem_conjgV (normsP nEG) // groupV; case/setIP: Ny. by apply: pgroupS (genS _) (pE _ _ Ex1 Ex1y); apply/subsetP => u /[!inE]. have [y1 Ny1 Py1]: exists2 y1, y1 \in 'N_E(D) & y1 \notin P. case sNN: ('N_<<B>>('N_<<B>>(D)) \subset 'N_<<B>>(D)). exists y0 => //; have By0: y0 \in <<B>> by rewrite mem_gen ?setU11. rewrite inE Ey0 -By0 -in_setI. by rewrite -['N__(D)](nilpotent_sub_norm (pgroup_nil pB)) ?subsetIl. case/subsetPn: sNN => z /setIP[Bz NNz]; rewrite inE Bz inE. case/subsetPn=> y; rewrite mem_conjg => Dzy Dy. have:= Dzy; rewrite {1}defD; do 2![case/setIP]=> _ Bzy Ezy. have Ey: y \in E by rewrite -(normsP nEG _ (subsetP sBG z Bz)) mem_conjg. have /setIP[By Ny]: y \in 'N_<<B>>(D). by rewrite -(normP NNz) mem_conjg inE Bzy ?(subsetP nDD). exists y; first by rewrite inE Ey. by rewrite defD 2!inE Ey By !andbT in Dy. have [y2 Ny2 Dy2]: exists2 y2, y2 \in 'N_(P :&: E)(D) & y2 \notin D. case sNN: ('N_P('N_P(D)) \subset 'N_P(D)). have [z /= Ez sEzP] := Sylow_Jsub sylP (genS sBE) pB. have Gz: z \in G by apply: subsetP Ez. have /subsetPn[y Bzy Dy]: ~~ (B :^ z \subset D). apply/negP; move/subset_leq_card; rewrite cardJg cardsU1. by rewrite {1}defD 2!inE (negPf Py0) ltnn. exists y => //; apply: subsetP Bzy. rewrite -setIA setICA subsetI sub_conjg (normsP nEG) ?groupV // sBE. have nilP := pgroup_nil (pHall_pgroup sylP). by rewrite -['N__(_)](nilpotent_sub_norm nilP) ?subsetIl // -gen_subG genJ. case/subsetPn: sNN => z /setIP[Pz NNz]; rewrite 2!inE Pz. case/subsetPn=> y Dzy Dy; exists y => //; apply: subsetP Dzy. rewrite -setIA setICA subsetI sub_conjg (normsP nEG) ?groupV //. by rewrite sDE -(normP NNz); rewrite conjSg subsetI sDP. by apply: subsetP Pz; apply: (subset_trans (pHall_sub sylP)). suff{Dy2} Dy2D: y2 |: D = D by rewrite -Dy2D setU11 in Dy2. apply: maxD; last by rewrite subsetUr. case/setIP: Ny2 => PEy2 Ny2; case/setIP: Ny1 => Ey1 Ny1. rewrite subUset sub1set PEy2 subsetI sDP sDE. apply/existsP; exists y1; rewrite inE Ey1 Py1; apply: pgroupS pN. rewrite genS // !subUset !sub1set !in_setI Ey1 Ny1. by case/setIP: PEy2 => _ ->; rewrite Ny2 subsetI sDE. 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)