Zulip Chat Archive

Hi all, I have a s : finset a for some a : Type and a function f : a → b, where (b : Type) [add_comm_monoid b], so I can consider the sum ∑ x in s, f x. I also have another function g: a → b and I now that $f = g$ on $s$ , but not in general. I want to prove that ∑ x in s, f x = ∑ x in s, g x. How can I prove this? It is something like a rw I guess, but I do not know how tell Lean to use the fact that $f = g$ on $s$ (actually I am not even able to write this in Lean, maybe something like x ∈ s → f x = g x, where x : a?). Thank you!

Anne Baanen (Oct 15 2020 at 12:42):

I think you want to apply finset.sum_congr.

Riccardo Brasca (Oct 15 2020 at 12:45):

Oh, thank you! For some reasons I tried to do it by myself without looking into the library.

Riccardo Brasca (Oct 15 2020 at 12:47):

Is there a reason of having in finset.sum_congr two finsets s1 and s2 with the assumption that s1 = s2?

Anne Baanen (Oct 15 2020 at 12:50):

I guess it's just to make it more general, making it possible to vary the set being summed.

Anne Baanen (Oct 15 2020 at 12:51):

But usually I need finset.sum_bij if s1 and s2 are not literally the same.

Johan Commelin (Oct 15 2020 at 12:56):

sum_bij is what you need if s1 and s2 are not finsets of the same type.

Johan Commelin (Oct 15 2020 at 12:56):

Note that there is even sum_bij_ne_zero which is the most awesome version of all (-;

Johan Commelin (Oct 15 2020 at 12:57):

And fintype.sum_congr if you are looking at two sums over a fintype (i.e. s1 = s2 = (univ : finset X))

Riccardo Brasca (Oct 15 2020 at 12:58):

Wow, sum_bij_ne_zero is scary :grinning:

Kevin Buzzard (Oct 15 2020 at 13:19):

@Riccardo Brasca the difficulty of some of this finite stuff was quite surprising to me. I am pretty sure that when I arrived on the scene in 2017 trying to do 1st year UG problem sheets, if all the machinery of finite sets and finite types hadn't been there I would have been completely lost and unable to use anything. But people like Mario had built this stuff before. How difficult can a finite set be? Well, data.finset was thousands of lines long in 2017, and it imported data.multiset which was also thousands of lines long -- I once printed out data.multiset onto 28 pages and would sit and read it in the bath trying to fathom out what was going on.

Riccardo Brasca (Oct 15 2020 at 13:20):

Yes, the machinery is quite confusing at the beginning, but I guess one gets used to it.

Kevin Buzzard (Oct 15 2020 at 13:20):

It was only much later that I realised that the point was not to see how it was built, it was to understand what the main definitions were (these files are 98% theorems)