proposition: Lemma simple_Alt5_base (T : finType) : #|T| = 5 -> simple 'Alt_T.
proof: Proof. move=> oT. have F1: #|'Alt_T| = 60 by apply: double_inj; rewrite -mul2n card_Alt oT. have FF (H : {group {perm T}}): H <| 'Alt_T -> H :<>: 1 -> 20 %| #|H|. - move=> Hh1 Hh3. have [x _]: exists x, x \in T by apply/existsP/eqP; rewrite oT. have F2 := Alt_trans T; rewrite oT /= in F2. have F3: [transitive 'Alt_T, on setT | 'P] by apply: ntransitive1 F2. have F4: [primitive 'Alt_T, on setT | 'P] by apply: ntransitive_primitive F2. case: (prim_trans_norm F4 Hh1) => F5. by case: Hh3; apply/trivgP; apply: subset_trans F5 (aperm_faithful _). have F6: 5 %| #|H| by rewrite -oT -cardsT (atrans_dvd F5). have F7: 4 %| #|H|. have F7: #|[set~ x]| = 4 by rewrite cardsC1 oT. case: (pickP [in [set~ x]]) => [y Hy | ?]; last by rewrite eq_card0 in F7. pose K := 'C_H[x | 'P]%G. have F8 : K \subset H by apply: subsetIl. pose Gx := 'C_('Alt_T)[x | 'P]%G. have F9: [transitive^2 Gx, on [set~ x] | 'P]. by rewrite -[[set~ x]]setTI -setDE stab_ntransitive ?inE. have F10: [transitive Gx, on [set~ x] | 'P]. exact: ntransitive1 F9. have F11: [primitive Gx, on [set~ x] | 'P]. exact: ntransitive_primitive F9. have F12: K \subset Gx by apply: setSI; apply: normal_sub. have F13: K <| Gx by rewrite /(K <| _) F12 normsIG // normal_norm. case: (prim_trans_norm F11 F13) => Ksub; last first. by apply: dvdn_trans (cardSg F8); rewrite -F7; apply: atrans_dvd Ksub. have F14: [faithful Gx, on [set~ x] | 'P]. apply/subsetP=> g; do 2![case/setIP] => Altg cgx cgx'. apply: (subsetP (aperm_faithful 'Alt_T)). rewrite inE Altg /=; apply/astabP=> z _. case: (z =P x) => [->|]; first exact: (astab1P cgx). by move/eqP=> nxz; rewrite (astabP cgx') ?inE //. have Hreg g (z : T): g \in H -> g z = z -> g = 1. have F15 h: h \in H -> h x = x -> h = 1. move=> Hh Hhx; have: h \in K by rewrite inE Hh; apply/astab1P. by rewrite (trivGP (subset_trans Ksub F14)) => /set1P. move=> Hg Hgz; have:= in_setT x; rewrite -(atransP F3 z) ?inE //. case/imsetP=> g1 Hg1 Hg2; apply: (conjg_inj g1); rewrite conj1g. apply: F15; last by rewrite Hg2 -permM mulKVg permM Hgz. by case/normalP: Hh1 => _ nH1; rewrite -(nH1 _ Hg1) memJ_conjg. clear K F8 F12 F13 Ksub F14. case: (Cauchy _ F6) => // h Hh /eqP Horder. have diff_hnx_x n: 0 < n -> n < 5 -> x != (h ^+ n) x. move=> Hn1 Hn2; rewrite eq_sym; apply/negP => HH. have: #[h ^+ n] = 5. rewrite orderXgcd // (eqP Horder). by move: Hn1 Hn2 {HH}; do 5 (case: n => [|n] //). have Hhd2: h ^+ n \in H by rewrite groupX. by rewrite (Hreg _ _ Hhd2 (eqP HH)) order1. pose S1 := [tuple x; h x; (h ^+ 3) x]. have DnS1: S1 \in 3.-dtuple(setT). rewrite inE memtE subset_all /= !inE /= !negb_or -!andbA /= andbT. rewrite -{1}[h]expg1 !diff_hnx_x // expgSr permM. by rewrite (inj_eq perm_inj) diff_hnx_x. pose S2 := [tuple x; h x; (h ^+ 2) x]. have DnS2: S2 \in 3.-dtuple(setT). rewrite inE memtE subset_all /= !inE /= !negb_or -!andbA /= andbT. rewrite -{1}[h]expg1 !diff_hnx_x // expgSr permM. by rewrite (inj_eq perm_inj) diff_hnx_x. case: (atransP2 F2 DnS1 DnS2) => g Hg [/=]. rewrite /aperm => Hgx Hghx Hgh3x. have h_g_com: h * g = g * h. suff HH: (g * h * g^-1) * h^-1 = 1 by rewrite -[h * g]mul1g -HH !gnorm. apply: (Hreg _ x); last first. by rewrite !permM -Hgx Hghx -!permM mulKVg mulgV perm1. rewrite groupM // ?groupV // (conjgCV g) mulgK -mem_conjg. by case/normalP: Hh1 => _ ->. have: (g * (h ^+ 2) * g ^-1) x = (h ^+ 3) x. rewrite !permM -Hgx. have ->: h (h x) = (h ^+ 2) x by rewrite /= permM. by rewrite {1}Hgh3x -!permM /= mulgV mulg1 -expgSr. rewrite commuteX // mulgK {1}[expgn]lock expgS permM -lock. by move/perm_inj=> eqxhx; case/eqP: (diff_hnx_x 1%N isT isT); rewrite expg1. by rewrite (@Gauss_dvd 4 5) // F7. apply/simpleP; split => [|H Hnorm]; first by rewrite trivg_card1 F1. case Hcard1: (#|H| == 1%N); move/eqP: Hcard1 => Hcard1. by left; apply: card1_trivg; rewrite Hcard1. right; case Hcard60: (#|H| == 60); move/eqP: Hcard60 => Hcard60. by apply/eqP; rewrite eqEcard Hcard60 F1 andbT; case/andP: Hnorm. have {Hcard1 Hcard60} Hcard20: #|H| = 20. have Hdiv: 20 %| #|H| by apply: FF => // HH; case Hcard1; rewrite HH cards1. case H20: (#|H| == 20); first exact/eqP. case: Hcard60; case/andP: Hnorm; move/cardSg; rewrite F1 => Hdiv1 _. by case/dvdnP: Hdiv H20 Hdiv1 => n ->; move: n; do 4!case=> //. have prime_5: prime 5 by []. have nSyl5: #|'Syl_5(H)| = 1%N. move: (card_Syl_dvd 5 H) (card_Syl_mod H prime_5). rewrite Hcard20; case: (card _) => // n Hdiv. move: (dvdn_leq (isT: (0 < 20)%N) Hdiv). by move: (n) Hdiv; do 20 (case=> //). case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS. have{} oS: #|S| = 5 by rewrite oS p_part Hcard20. suff: 20 %| #|S| by rewrite oS. apply: FF => [|S1]; last by rewrite S1 cards1 in oS. apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS. rewrite subEproper; apply/norP=> [[nQS _]]; move: nSyl5. rewrite (cardsD1 S) (cardsD1 Q) 4!{1}inE nQS !pHallE sQH sSH Hcard20 p_part. by rewrite (card_isog isoQS) oS. 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)