proposition: Lemma stab_tuple_prod : 'C[wp | pact] = (\prod_(x : seq_sub w) Sym_group [set i | tnth w i == val x])%G.
proof: Proof. Proof using. have Htriv : trivIset [set [set i | tnth w i == val x] | x : seq_sub w]. apply/trivIsetP => /= X Y. move=> /imsetP[/= [x Hx _ /= ->{X}]]. move=> /imsetP[/= [y Hy _ /= ->{Y}]] Hneq. rewrite -setI_eq0; apply/eqP/setP => /= i. rewrite !inE; apply/negP => /andP[/eqP -> /eqP Hxy]. by move: Hneq; rewrite Hxy eq_refl. apply/eqP; rewrite bigprodGE eqEsubset; apply/andP; split. - apply/subsetP => /= s. move/astabP/(_ wp); rewrite inE eq_refl => /(_ isT) Ht. rewrite -(perm_decE (s := s) Htriv); first last. + apply/astabP => /= CS /imsetP[/= x _ ->{CS}]. apply/astab1P; rewrite astab1_set. rewrite !inE /=; apply/subsetP => j. rewrite !inE => /eqP <-. by rewrite -{1}[w]/(val wp) -Ht tnth_mktuple permK. + apply/subsetP => /= i _; apply/bigcupP => /=. exists [set i0 | tnth w i0 == tnth w i]; last by rewrite inE. by apply/imsetP => /=; exists (SeqSub (mem_tnth i w)) => //=. apply group_prod => /= u /imsetP[/= X]. move=> /imsetP[x Hx ->{X} ->{u}]; apply/mem_gen. apply/bigcupP; exists x => //. by rewrite inE; exact: restr_perm_on. - rewrite gen_subG; apply/subsetP => /= s /bigcupP[/= x _] Hs. rewrite !inE /=; apply/subsetP => j; rewrite !inE => /eqP ->{j}. apply/eqP/val_inj/eq_from_tnth => /= i. rewrite tnth_mktuple. case: (boolP (tnth w i == val x)) => Hl0. + move: Hs; rewrite inE => /im_perm_on/setP/(_ i). rewrite !inE Hl0 => /imsetP[/= j]. rewrite inE => /eqP H {1}->. by rewrite (eqP Hl0) permK. + move: Hs => /groupVr; rewrite inE /= => /out_perm -> //. by rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles