Reverse sum order

Stream: new members

[Emma R. Hasson]

Still working with sums- I think I'm supposed to use finset.sum_sigma here, but I'm not sure how to apply it.

example (f : ℝ → ℝ → ℝ) (s t : finset ℝ) :
  ∑ x in s, ∑ y in t, f x y =  ∑ y in t, ∑ x in s, f x y  :=
begin
  sorry
end

[Ruben Van de Velde]

I think you want sum_comm, not sum_sigma

[Ruben Van de Velde]

sum_sigma is about a sum over a sigma/disjoint union type