proposition: Lemma partition_big_undup_map (p : seq A) (f : A -> B) : forall g, uniq p -> \big[M/idx]_(i <- p) g i = \big[M/idx]_(r <- undup (map f p)) \big[M/idx]_(i <- p | f i == r) (g i).
proof: Proof. move Hn : (undup (map f (p))) => n. elim: n p f Hn => [p f H F ? | b bs IH p f H F ?]. rewrite big_nil. suff -> : p = [::] by rewrite big_nil. move/undup_nil : H => /(congr1 size) /=; rewrite size_map. by move/eqP; rewrite size_eq0 => /eqP. rewrite big_cons. have [h [t [H1 [H2 H3]]]] : exists h t, perm_eq p (h ++ t) /\ undup (map f h) = [:: b] /\ undup (map f t) = bs. exact: undup_perm. transitivity (\big[M/idx]_(i <- h ++ t) F i); first exact: perm_big. transitivity (M (\big[M/idx]_(i <- h ++ t | f i == b) F i) (\big[M/idx]_(j <- bs) \big[M/idx]_(i <- h ++ t | f i == j) F i)); last first. congr (M _ _). by apply: perm_big; rewrite perm_sym. by apply eq_bigr => b0 _ /=; apply: perm_big; rewrite perm_sym. have -> : \big[M/idx]_(j <- bs) \big[M/idx]_(i <- h ++ t | f i == j) F i = \big[M/idx]_(j <- bs) \big[M/idx]_(i <- t | f i == j) F i. rewrite [in LHS]big_seq [in RHS]big_seq /=. apply/esym/eq_bigr => b0 b0bs. rewrite big_cat /=. rewrite (_ : \big[M/idx]_(i0 <- h | f i0 == b0) F i0 = idx) ?Monoid.add0m//. transitivity (\big[M/idx]_(i0 <- h | false) F i0); last by rewrite big_pred0. rewrite big_seq_cond; apply eq_bigl => /= a. apply/negP => /andP[ah /eqP fai]; subst b0. have fab : f a \in [:: b]. have H' : f a \in map f h by apply/mapP; exists a. have : f a \in undup (map f h) by rewrite mem_undup. by rewrite H2. have : uniq (b :: bs) by rewrite -H undup_uniq. move: fab; rewrite /= in_cons in_nil orbC /= => /eqP ?; subst b. by rewrite b0bs. rewrite -IH //; last first. have : uniq (h ++ t) by rewrite -(perm_uniq H1). by rewrite cat_uniq => /and3P[]. suff -> : \big[M/idx]_(i <- h ++ t | f i == b) F i = \big[M/idx]_(i <- h) F i. by rewrite big_cat. rewrite big_cat /=. have -> : \big[M/idx]_(i <- t | f i == b) F i = idx. transitivity (\big[M/idx]_(i0 <- t | false) F i0); last by rewrite big_pred0. rewrite big_seq_cond; apply eq_bigl => /= a. apply/negP => /andP[ta /eqP fab]; subst b. have fabs : f a \in bs. have : f a \in undup (map f t) by rewrite mem_undup; apply/mapP; exists a. by rewrite H3. have : uniq (f a :: bs) by rewrite -H undup_uniq. by rewrite /= fabs. rewrite Monoid.addm0 big_seq_cond /=. apply/esym. rewrite big_seq /=; apply congr_big => //= a. case/boolP : (a \in h) => ah //=; apply/esym. have : f a \in [:: b] by rewrite -H2 mem_undup; apply/mapP; exists a. by rewrite in_cons /= in_nil orbC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext