proposition: Lemma big_distr_big_dep (I J : finType) j0 (P : pred I) (Q : I -> pred J) F : \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q i j) F i j = \big[+%M/0]_(f in pfamily j0 P Q) \big[*%M/1]_(i | P i) F i (f i).
proof: Proof. pose fIJ := {ffun I -> J}; pose Pf := pfamily j0 (_ : seq I) Q. have [r big_r [Ur mem_r] _] := big_enumP P. symmetry; transitivity (\big[+%M/0]_(f in Pf r) \big[*%M/1]_(i <- r) F i (f i)). by apply: eq_big => // f; apply: eq_forallb => i; rewrite /= mem_r. rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr]. rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f. apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE. by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df. case/andP=> /negbTE nri; rewrite big_cons big_distrl => {}/IHr<-. rewrite (partition_big (fun f : fIJ => f i) (Q i)) => [|f]; last first. by move/familyP/(_ i); rewrite /= inE /= eqxx. pose seti j (f : fIJ) := [ffun k => if k == i then j else f k]. apply: eq_bigr => j Qij. rewrite (reindex_onto (seti j) (seti j0)) => [|f /andP[_ /eqP fi]]; last first. by apply/ffunP=> k; rewrite !ffunE; case: eqP => // ->. rewrite big_distrr; apply: eq_big => [f | f eq_f]; last first. rewrite big_cons ffunE eqxx !big_seq; congr (_ * _). by apply: eq_bigr => k; rewrite ffunE; case: eqP nri => // -> ->. rewrite !ffunE !eqxx andbT; apply/andP/familyP=> /= [[Pjf fij0] k | Pff]. have /[!(ffunE, inE)] := familyP Pjf k; case: eqP => // -> _. by rewrite nri -(eqP fij0) !ffunE !inE !eqxx. split; [apply/familyP | apply/eqP/ffunP] => k; have /[!(ffunE, inE)]:= Pff k. by case: eqP => // ->. by case: eqP => // ->; rewrite nri /= => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)