# Zulip Chat Archive

## 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, but`ext`

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

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

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`

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

Then apologies for being misleading

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

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