proposition: Lemma not_simple_Alt_4 (T : finType) : #|T| = 4 -> ~~ simple 'Alt_T.
proof: Proof. move=> oT; set A := 'Alt_T. have oA: #|A| = 12 by apply: double_inj; rewrite -mul2n card_Alt oT. suffices [p]: exists p, [/\ prime p, 1 < #|A|`_p < #|A| & #|'Syl_p(A)| == 1%N]. case=> p_pr pA_int; rewrite /A; case/normal_sylowP=> P; case/pHallP. rewrite /= -/A => sPA pP nPA; apply/simpleP=> [] [_]; rewrite -pP in pA_int. by case/(_ P)=> // defP; rewrite defP oA ?cards1 in pA_int. have: #|'Syl_3(A)| \in filter [pred d | d %% 3 == 1%N] (divisors 12). by rewrite mem_filter -dvdn_divisors //= -oA card_Syl_dvd ?card_Syl_mod. rewrite /= oA mem_seq2 orbC. case/predU1P=> [oQ3|]; [exists 2 | exists 3]; split; rewrite ?p_part //. pose A3 := [set x : {perm T} | #[x] == 3]; suffices oA3: #|A :&: A3| = 8. have sQ2 P: P \in 'Syl_2(A) -> P :=: A :\: A3. rewrite inE pHallE oA p_part -natTrecE /= => /andP[sPA /eqP oP]. apply/eqP; rewrite eqEcard -(leq_add2l 8) -{1}oA3 cardsID oA oP. rewrite andbT subsetD sPA; apply/exists_inP=> -[x] /= Px. by rewrite inE => /eqP ox; have:= order_dvdG Px; rewrite oP ox. have [/= P sylP] := Sylow_exists 2 [group of A]. rewrite -(([set P] =P 'Syl_2(A)) _) ?cards1 // eqEsubset sub1set inE sylP. by apply/subsetP=> Q sylQ; rewrite inE -val_eqE /= !sQ2 // inE. rewrite -[8]/(4 * 2)%N -{}oQ3 -sum1_card -sum_nat_const. rewrite (partition_big (fun x => <[x]>%G) [in 'Syl_3(A)]) => [|x]; last first. by case/setIP=> Ax; rewrite /= !inE pHallE p_part cycle_subG Ax oA. apply: eq_bigr => Q; rewrite inE pHallE oA p_part -?natTrecE //=. case/andP=> sQA /eqP oQ; have:= oQ. rewrite (cardsD1 1) group1 -sum1_card => [[/= <-]]; apply: eq_bigl => x. rewrite setIC -val_eqE /= 2!inE in_setD1 -andbA -{4}[x]expg1 -order_dvdn dvdn1. apply/and3P/andP=> [[/eqP-> _ /eqP <-] | [ntx Qx]]; first by rewrite cycle_id. have:= order_dvdG Qx; rewrite oQ dvdn_divisors // mem_seq2 (negPf ntx) /=. by rewrite eqEcard cycle_subG Qx (subsetP sQA) // oQ /order => /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype tuple tuple bigop prime finset fingroup) mathcomp(morphism perm automorphism quotient action cyclic) mathcomp(pgroup gseries sylow primitive_action)