## Stream: new members

### Topic: Rw inside a sum

#### Riccardo Brasca (Oct 15 2020 at 12:41):

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)

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

And probably sooner or later I will have to read it in details too.

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

and to start to understand what kind of things are available

#### Kevin Buzzard (Oct 15 2020 at 13:21):

Here is the way to read a file in mathilb. First, check to see if there is a module docstring. If there is, then read all of that first.

#### Kevin Buzzard (Oct 15 2020 at 13:21):

And if there isn't then I guess you could even just make one yourself after you finished reading it.

#### Kevin Buzzard (Oct 15 2020 at 13:22):

Secondly try and find all the definitions and all the instances (use search functionality of your viewer)

#### Kevin Buzzard (Oct 15 2020 at 13:22):

Hopefully each one should have a docstring. They should tell you the main objects you're working with in this file.

#### Kevin Buzzard (Oct 15 2020 at 13:23):

Then scan the theorems to work out the normal form for each new concept, i.e how things are expressed on the right hand side of simp lemmas.

#### Kevin Buzzard (Oct 15 2020 at 13:23):

because simp moves things from left to right

#### Kevin Buzzard (Oct 15 2020 at 13:23):

and then scan the theorems, you probably won't see anything surprising, so skip the proofs.

#### Kevin Buzzard (Oct 15 2020 at 13:24):

Then if there wasn't a module docstring, pop back to the top and write one.

#### Scott Morrison (Oct 15 2020 at 21:28):

Oh! There is a tactic for this!

#### Scott Morrison (Oct 15 2020 at 21:30):

https://leanprover-community.github.io/mathlib_docs/tactics.html#apply_congr

#### Riccardo Brasca (Oct 16 2020 at 14:27):

Very nice, this is exactly what I wanted! :)

Last updated: May 08 2021 at 18:17 UTC