proposition: Lemma critical_extraspecial R S : p.-group R -> S \subset R -> extraspecial S -> [~: S, R] \subset S^`(1) -> S \* 'C_R(S) = R.
proof: Proof. move=> pR sSR esS sSR_S'; have [[defPhi defS'] _] := esS. have [pS [sPS nPS]] := (pgroupS sSR pR, andP (Phi_normal S : 'Phi(S) <| S)). have{esS} oZS: #|'Z(S)| = p := card_center_extraspecial pS esS. have nSR: R \subset 'N(S) by rewrite -commg_subl (subset_trans sSR_S') ?der_sub. have nsCR: 'C_R(S) <| R by rewrite (normalGI nSR) ?cent_normal. have nCS: S \subset 'N('C_R(S)) by rewrite cents_norm // centsC subsetIr. rewrite cprodE ?subsetIr //= -{2}(quotientGK nsCR) normC -?quotientK //. congr (_ @*^-1 _); apply/eqP; rewrite eqEcard quotientS //=. rewrite -(card_isog (second_isog nCS)) setIAC (setIidPr sSR) /= -/'Z(S) -defPhi. rewrite -ker_conj_aut (card_isog (first_isog_loc _ nSR)) //=; set A := _ @* R. have{pS} abelSb := Phi_quotient_abelem pS; have [pSb cSSb _] := and3P abelSb. have [/= Xb defSb oXb] := grank_witness (S / 'Phi(S)). pose X := (repr \o val : coset_of _ -> gT) @: Xb. have sXS: X \subset S; last have nPX := subset_trans sXS nPS. apply/subsetP=> x; case/imsetP=> xb Xxb ->; have nPx := repr_coset_norm xb. rewrite -sub1set -(quotientSGK _ sPS) ?sub1set ?quotient_set1 //= sub1set. by rewrite coset_reprK -defSb mem_gen. have defS: <<X>> = S. apply: Phi_nongen; apply/eqP; rewrite eqEsubset join_subG sPS sXS -joing_idr. rewrite -genM_join sub_gen // -quotientSK ?quotient_gen // -defSb genS //. apply/subsetP=> xb Xxb; apply/imsetP; rewrite (setIidPr nPX). by exists (repr xb); rewrite /= ?coset_reprK //; apply: imset_f. pose f (a : {perm gT}) := [ffun x => if x \in X then x^-1 * a x else 1]. have injf: {in A &, injective f}. move=> _ _ /morphimP[y nSy Ry ->] /morphimP[z nSz Rz ->]. move/ffunP=> eq_fyz; apply: (@eq_Aut _ S); rewrite ?Aut_aut //= => x Sx. rewrite !norm_conj_autE //; apply: canRL (conjgKV z) _; rewrite -conjgM. rewrite /conjg -(centP _ x Sx) ?mulKg {x Sx}// -defS cent_gen -sub_cent1. apply/subsetP=> x Xx; have Sx := subsetP sXS x Xx. move/(_ x): eq_fyz; rewrite !ffunE Xx !norm_conj_autE // => /mulgI xy_xz. by rewrite cent1C inE conjg_set1 conjgM xy_xz conjgK. have sfA_XS': f @: A \subset pffun_on 1 X S^`(1). apply/subsetP=> _ /imsetP[_ /morphimP[y nSy Ry ->] ->]. apply/pffun_onP; split=> [|_ /imageP[x /= Xx ->]]. by apply/subsetP=> x; apply: contraNT => /[!ffunE]/negPf->. have Sx := subsetP sXS x Xx. by rewrite ffunE Xx norm_conj_autE // (subsetP sSR_S') ?mem_commg. rewrite -(card_in_imset injf) (leq_trans (subset_leq_card sfA_XS')) // defS'. rewrite card_pffun_on (card_pgroup pSb) -rank_abelem -?grank_abelian // -oXb. by rewrite -oZS ?leq_pexp2l ?cardG_gt0 ?leq_imset_card. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)