proposition: Lemma simple_Alt5 (T : finType) : #|T| >= 5 -> simple 'Alt_T.
proof: Proof. suff F1 n: #|T| = n + 5 -> simple 'Alt_T by move/subnK/esym/F1. elim: n T => [| n Hrec T Hde]; first exact: simple_Alt5_base. have oT: 5 < #|T| by rewrite Hde addnC. apply/simpleP; split=> [|H Hnorm]; last have [Hh1 nH] := andP Hnorm. rewrite trivg_card1 -[#|_|]half_double -mul2n card_Alt Hde addnC //. by rewrite addSn factS mulnC -(prednK (fact_gt0 _)). case E1: (pred0b T); first by rewrite /pred0b in E1; rewrite (eqP E1) in oT. case/pred0Pn: E1 => x _; have Hx := in_setT x. have F2: [transitive^4 'Alt_T, on setT | 'P]. by apply: ntransitive_weak (Alt_trans T); rewrite -(subnKC oT). have F3 := ntransitive1 (isT: 0 < 4) F2. have F4 := ntransitive_primitive (isT: 1 < 4) F2. case Hcard1: (#|H| == 1%N); move/eqP: Hcard1 => Hcard1. by left; apply: card1_trivg; rewrite Hcard1. right; case: (prim_trans_norm F4 Hnorm) => F5. by rewrite (trivGP (subset_trans F5 (aperm_faithful _))) cards1 in Hcard1. case E1: (pred0b (predD1 T x)). rewrite /pred0b in E1; move: oT. by rewrite (cardD1 x) (eqP E1); case: (T x). case/pred0Pn: E1 => y Hdy; case/andP: (Hdy) => diff_x_y Hy. pose K := 'C_H[x | 'P]%G. have F8: K \subset H by apply: subsetIl. pose Gx := 'C_('Alt_T)[x | 'P]. have F9: [transitive^3 Gx, on [set~ x] | 'P]. by rewrite -[[set~ x]]setTI -setDE stab_ntransitive ?inE. have F10: [transitive Gx, on [set~ x] | 'P]. by apply: ntransitive1 F9. have F11: [primitive Gx, on [set~ x] | 'P]. by apply: ntransitive_primitive F9. have F12: K \subset Gx by rewrite setSI // normal_sub. have F13: K <| Gx by apply/andP; rewrite normsIG. have:= prim_trans_norm F11; case/(_ K) => //= => Ksub; last first. have F14: Gx * H = 'Alt_T by apply/(subgroup_transitiveP _ _ F3). have: simple Gx. by rewrite (isog_simple (rfd_iso x)) Hrec //= card_sig cardC1 Hde. case/simpleP=> _ simGx; case/simGx: F13 => /= HH2. case Ez: (pred0b (predD1 (predD1 T x) y)). move: oT; rewrite /pred0b in Ez. by rewrite (cardD1 x) (cardD1 y) (eqP Ez) inE /= inE /= diff_x_y. case/pred0Pn: Ez => z; case/andP => diff_y_z Hdz. have [diff_x_z Hz] := andP Hdz. have: z \in [set~ x] by rewrite !inE. rewrite -(atransP Ksub y) ?inE //; case/imsetP => g. rewrite /= HH2 inE; move/eqP=> -> HH4. by case/negP: diff_y_z; rewrite HH4 act1. by rewrite /= -F14 -[Gx]HH2 (mulSGid F8). have F14: [faithful Gx, on [set~ x] | 'P]. apply: subset_trans (aperm_faithful 'Sym_T); rewrite subsetI subsetT. apply/subsetP=> g; do 2![case/setIP]=> _ cgx cgx'; apply/astabP=> z _ /=. case: (z =P x) => [->|]; first exact: (astab1P cgx). by move/eqP=> zx; rewrite [_ g](astabP cgx') ?inE. have Hreg g z: 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 [K](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 rewrite memJ_norm ?(subsetP nH). clear K F8 F12 F13 Ksub F14. have Hcard: 5 < #|H|. apply: (leq_trans oT); apply: dvdn_leq; first exact: cardG_gt0. by rewrite -cardsT (atrans_dvd F5). case Eh: (pred0b [predD1 H & 1]). by move: Hcard; rewrite /pred0b in Eh; rewrite (cardD1 1) group1 (eqP Eh). case/pred0Pn: Eh => h; case/andP => diff_1_h /= Hh. case Eg: (pred0b (predD1 (predD1 [predD1 H & 1] h) h^-1)). move: Hcard; rewrite ltnNge; case/negP. rewrite (cardD1 1) group1 (cardD1 h) (cardD1 h^-1) (eqnP Eg). by do 2!case: (_ \in _). case/pred0Pn: Eg => g; case/andP => diff_h1_g; case/andP => diff_h_g. case/andP => diff_1_g /= Hg. case diff_hx_x: (h x == x). by case/negP: diff_1_h; apply/eqP; apply: (Hreg _ _ Hh (eqP diff_hx_x)). case diff_gx_x: (g x == x). case/negP: diff_1_g; apply/eqP; apply: (Hreg _ _ Hg (eqP diff_gx_x)). case diff_gx_hx: (g x == h x). case/negP: diff_h_g; apply/eqP; symmetry; apply: (mulIg g^-1); rewrite gsimp. apply: (Hreg _ x); first by rewrite groupM // groupV. by rewrite permM -(eqP diff_gx_hx) -permM mulgV perm1. case diff_hgx_x: ((h * g) x == x). case/negP: diff_h1_g; apply/eqP; apply: (mulgI h); rewrite !gsimp. by apply: (Hreg _ x); [apply: groupM | apply/eqP]. case diff_hgx_hx: ((h * g) x == h x). case/negP: diff_1_g; apply/eqP. by apply: (Hreg _ (h x)) => //; apply/eqP; rewrite -permM. case diff_hgx_gx: ((h * g) x == g x). by case/idP: diff_hx_x; rewrite -(can_eq (permK g)) -permM. case Ez: (pred0b (predD1 (predD1 (predD1 (predD1 T x) (h x)) (g x)) ((h * g) x))). - move: oT; rewrite /pred0b in Ez. rewrite (cardD1 x) (cardD1 (h x)) (cardD1 (g x)) (cardD1 ((h * g) x)). by rewrite (eqP Ez) addnC; do 3!case: (_ x \in _). case/pred0Pn: Ez => z. case/and5P=> diff_hgx_z diff_gx_z diff_hx_z diff_x_z /= Hz. pose S1 := [tuple x; h x; g x; z]. have DnS1: S1 \in 4.-dtuple(setT). rewrite inE memtE subset_all -!andbA !negb_or /= !inE !andbT. rewrite -!(eq_sym z) diff_gx_z diff_x_z diff_hx_z. by rewrite !(eq_sym x) diff_hx_x diff_gx_x eq_sym diff_gx_hx. pose S2 := [tuple x; h x; g x; (h * g) x]. have DnS2: S2 \in 4.-dtuple(setT). rewrite inE memtE subset_all -!andbA !negb_or /= !inE !andbT !(eq_sym x). rewrite diff_hx_x diff_gx_x diff_hgx_x. by rewrite !(eq_sym (h x)) diff_gx_hx diff_hgx_hx eq_sym diff_hgx_gx. case: (atransP2 F2 DnS1 DnS2) => k Hk [/=]. rewrite /aperm => Hkx Hkhx Hkgx Hkhgx. have h_k_com: h * k = k * h. suff HH: (k * h * k^-1) * h^-1 = 1 by rewrite -[h * k]mul1g -HH !gnorm. apply: (Hreg _ x); last first. by rewrite !permM -Hkx Hkhx -!permM mulKVg mulgV perm1. by rewrite groupM // ?groupV // (conjgCV k) mulgK -mem_conjg (normsP nH). have g_k_com: g * k = k * g. suff HH: (k * g * k^-1) * g^-1 = 1 by rewrite -[g * k]mul1g -HH !gnorm. apply: (Hreg _ x); last first. by rewrite !permM -Hkx Hkgx -!permM mulKVg mulgV perm1. by rewrite groupM // ?groupV // (conjgCV k) mulgK -mem_conjg (normsP nH). have HH: (k * (h * g) * k ^-1) x = z. by rewrite 2!permM -Hkx Hkhgx -permM mulgV perm1. case/negP: diff_hgx_z. rewrite -HH !mulgA -h_k_com -!mulgA [k * _]mulgA. by rewrite -g_k_com -!mulgA mulgV mulg1. 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)