proposition: Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x : {on SimplPred P, bijective h} -> \big[cprod/1]_(i | P i) A i = G -> {in SimplPred P, forall i, x i \in A i} -> \prod_(i | P i) x i = \prod_(j | P (h j)) x (h j).
proof: Proof. case=> h1 hK h1K defG Ax; have [e big_e [Ue mem_e] _] := big_enumP P. rewrite -!big_e in defG *; rewrite -(big_map h P x) -[RHS]big_filter filter_map. apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_e => /Ax. have [r _ [Ur /= mem_r] _] := big_enumP; apply: uniq_perm Ue _ _ => [|i]. by rewrite map_inj_in_uniq // => i j; rewrite !mem_r ; apply: (can_in_inj hK). rewrite mem_e; apply/idP/mapP=> [Pi|[j r_j ->]]; last by rewrite -mem_r. by exists (h1 i); rewrite ?mem_r h1K. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)