## Stream: new members

### Topic: Extensionality for big operators

#### Justus Springer (Apr 23 2021 at 17:01):

So I'm in a situation where I want to prove that two sums are equal, knowing that for each index, the summands are equal. Like this:

import data.finset

open_locale big_operators

variables {α : Type*} {β : Type*} [add_comm_monoid β]

lemma foo (s : finset α) (f g : α → β) (h : ∀ x ∈ s, f x = g x) :
∑ (x : α) in s, f x = ∑ (x : α) in s, g x :=
begin
sorry
end


Seems like a pretty trivial task, however I can't seem to find the right lemma to prove this... Initially this felt like some kind of extensionality lemma, butext gives the error message: only constants and Pi types are supported: β. Using congr makes progress, but it would require me to prove f x = g x for all values x : α, but I only know it for elements of s.

I've been stuck here for quite some time now, any help is much appreciated!

#### Johan Commelin (Apr 23 2021 at 17:04):

finset.sum_congr rfl h

#### Patrick Massot (Apr 23 2021 at 17:05):

Johan is wrong, he wanted to write library_search.

#### Patrick Massot (Apr 23 2021 at 17:06):

That's really important to know.

#### Justus Springer (Apr 23 2021 at 17:54):

I'm amazed that I didn't find this!
Thanks

Or congr' 1

#### Yakov Pechersky (Apr 23 2021 at 17:55):

To prevent congr from doing too much

#### Justus Springer (Apr 23 2021 at 17:57):

Yakov Pechersky said:

Or congr' 1

That one doesn't work for me, it produces the goal (λ (x : α), f x) = λ (x : α), g x

#### Justus Springer (Apr 23 2021 at 17:58):

I only know f x = g x for x ∈ s

No problem :)

#### Patrick Massot (Apr 23 2021 at 17:59):

Justus Springer said:

I'm amazed that I didn't find this!
Thanks

library_search is really a fundamental tactic, especially after you made the effort of stating a clean general lemma as you did.

#### Kevin Buzzard (Apr 23 2021 at 18:02):

finset.sum_congr rfl is such a common idiom, and it's really hard to find: it's like one of those secrets which gets passed around. It took me a while to understand what a congr lemma was, but once I'd got the hang of it it really started opening doors for me, e.g. I could guess what the logic lemmas and_congr and forall_congr were going to say and use them without having to trouble library_search.

#### Eric Wieser (Apr 23 2021 at 18:16):

The nice thing about docs#finsum is congr just works!

#### Justus Springer (Apr 23 2021 at 18:57):

Patrick Massot said:

library_search is really a fundamental tactic, especially after you made the effort of stating a clean general lemma as you did.

Good tip! Extracting the general statement I'm looking for and then throwing library_search at it seems like a great strategy

#### Justus Springer (Apr 23 2021 at 18:59):

Kevin Buzzard said:

finset.sum_congr rfl is such a common idiom, and it's really hard to find: it's like one of those secrets which gets passed around. It took me a while to understand what a congr lemma was, but once I'd got the hang of it it really started opening doors for me, e.g. I could guess what the logic lemmas and_congr and forall_congr were going to say and use them without having to trouble library_search.

I guess haven't internalized yet what a congr lemma is, I was thinking ext for some reason

#### Kevin Buzzard (Apr 23 2021 at 19:16):

ext gets you from \forall x, f x = g x to f = g. But congr gets you from \forall x, f x = g x to [some stuff I make with some f x values] = [some stuff I make with some g x values].

#### Eric Wieser (Apr 23 2021 at 19:22):

Where "from X to Y" there means "your goal was Y and is now X"

#### Eric Wieser (Apr 23 2021 at 19:23):

congr turns foo x1 y1 = foo x2 y2 into two goals, x1 = x2 and y1 = y2

#### Kevin Buzzard (Apr 23 2021 at 19:58):

We mathematicians go forwards :-)

#### Scott Morrison (Apr 23 2021 at 23:50):

There's also the little used tactic#apply_congr, which was designed for rewriting inside big operators when you need the membership hypothesis.

Last updated: Dec 20 2023 at 11:08 UTC