Access summation hypothesis in conv

Stream: Is there code for X?

[Dion Leijnse]

Hello,

Suppose we have a type X, an A : Finset X and a function f : X → Nat. We can then take ∑ x ∈ A, f x. If I want to prove something about this, using a hypothesis of the form h : x ∈ A → Prop where this Prop says something about f, then a natural strategy seems to use conv => arg 2 to move to the summand of the sum and then useh. However, when I do this, I lose the assumption x ∈ A, and only see the information that x is of type X. So my question is: is there a way in conv mode to move within the sum and not lose the information that x ∈ A?

[Ruben Van de Velde]

docs#Finset.sum_congr might be helpful

[Dion Leijnse]

Thanks!