Extensionality for big operators

Stream: new members

[Justus Springer]

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]

finset.sum_congr rfl h

[Patrick Massot]

Johan is wrong, he wanted to write library_search.

[Patrick Massot]

That's really important to know.

[Justus Springer]

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

[Yakov Pechersky]

Or congr' 1

[Yakov Pechersky]

To prevent congr from doing too much

[Justus Springer]

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]

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

[Yakov Pechersky]

Then apologies for being misleading

[Justus Springer]

No problem :)

[Patrick Massot]

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]

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]

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

[Justus Springer]

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]

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]

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]

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

[Eric Wieser]

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

[Kevin Buzzard]

We mathematicians go forwards :-)

[Scott Morrison]

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