Pushing indicator variables in in sum

Stream: Is there code for X?

[Christoph Spiegel]

Hi, what is the correct way of pushing a dependency in a summation to the summand like∑ x ∈ S, c = ∑ x : α, c * (if x ∈ S then 1 else 0) , where S : Finset α? Is an if-else statement even the correct way of modelling this? The goal is to swap summands with Finset.sum_comm.

[Bhavik Mehta]

That looks like how I'd do it, and simp closes that goal for me.

[Christoph Spiegel]

Bhavik Mehta said:

That looks like how I'd do it, and simp closes that goal for me.

True, simp closes it. Not sure how I missed that. But good to know that the if-else formulation is not a hacky workaround!