proposition: Lemma partition_big_preimset h (B : {set J}) F : \big[aop/idx]_(i in h @^-1: B) F i = \big[aop/idx]_(j in B) \big[aop/idx]_(i in I | h i == j) F i.
proof: Proof. have HA : [disjoint B :&: [set h x | x in I] & B :\: [set h x | x in I]] by rewrite -setI_eq0 -setIA setIDA [in _ :&: B]setIC -setIDA setDv !setI0. have Hha : [disjoint h @^-1: (B :&: [set h x | x in I]) & h @^-1: (B :\: [set h x | x in I])]. rewrite -setI_eq0 -preimsetI. suff : [disjoint B :&: [set h x | x in I] & B :\: [set h x | x in I]]. by rewrite -setI_eq0; move/eqP => ->; rewrite preimset0. by []. rewrite -(setID B (h @: I)) /= preimsetU. under eq_bigl do rewrite in_setU. rewrite bigU //. under [in RHS]eq_bigl do rewrite in_setU. rewrite bigU //. have -> : h @^-1: (B :\: [set h x | x in I]) = set0. apply/setP/subset_eqP/andP; rewrite sub0set; split => //. apply/subsetP=> i; rewrite !inE; case/andP. move/imsetP=> H _; rewrite boolp.falseE; apply: H. by exists i; rewrite ?inE. rewrite big_set0 Monoid.mulm1. have -> : \big[aop/idx]_(x in B :\: [set h x | x in I]) \big[aop/idx]_(i | h i == x) F i = \big[aop/idx]_(x in B :\: [set h x | x in I]) idx. apply eq_bigr => j. rewrite inE; case/andP => Hj Hj'. apply big_pred0 => i. apply/negP => /eqP hij. move: Hj; rewrite -hij. move/imsetP; apply. by exists i. rewrite big1_eq Monoid.mulm1. set B' := B :&: [set h x | x in I]. set A := h @^-1: B'. have -> : B' = h @: A by rewrite imset_preimset //; apply subsetIr. have Hright j : j \in h @: A -> \big[aop/idx]_(i in I | h i == j) F i = \big[aop/idx]_(i in A | h i == j) F i. move=> Hj; apply eq_bigl => i; apply andb_id2r; move/eqP => hij. move: Hj; rewrite -hij !inE. case/imsetP => x; rewrite /A /B' !inE => /andP [H H0] ->. by rewrite H H0. rewrite [in RHS](eq_bigr _ Hright). exact: partition_big_imset. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext