Compare sums ssreflect

Question

I am aiming to say that if we have

sum(a) = sum(b)

then

a = b.

What would be the suitable tactic to do this, if the goal looks like this:

\big[Radd_comoid/0]_(i <- fin_img (A:=U) (B:=R_eqType) X)
   Radd_comoid
     (Pr P F * (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: F) / Pr P F))
     (Pr P (~: F) *
      (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: ~: F) / Pr P (~: F))) =
\sum_(u in U) X u * `p_ X u

Editted. The context contains:

X: {RV (P) -> (R)}
F: {set U}
H: 0 < Pr P F
H0: Pr P F < 1

The goal after rewrite /=. looks like this:

\big[Rplus/0]_(i <- fin_img (A:=U) (B:=R_eqType) X)
   (Pr P F * (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: F) / Pr P F) +
    Pr P (~: F) *
    (i * Pr P (finset (T:=U) (preim X (pred1 i)) :&: ~: F) / Pr P (~: F))) =
\sum_(u in U) X u * `p_ X u

Answer 1

If it is true, you probably need to use sum_parti_finType on the right hand side and try to identify the general terms of the summation using eq_bigr. The general term of the left hand side can be simplified using mulrC mulfVK (or something like this) on both sides of the +. And then identify a sum of probabilities with the probability of the disjoint union. Anyway, it's not just "a tactic"...