## Stream: new members

### Topic: bsum ext

#### Damiano Testa (Feb 27 2021 at 12:19):

Dear All,

in the #mwe below, I would like to get Lean to tell me that the sums are equal if their terms are equal. However, if I use congr, Lean seems to forget that the indexing set is restricted to c.support, which in my actual situation is important, since only the i : ι satisfying i ∈ c.support are equal.

Is there an ext for the sum that will remember this and produce a goal such as ∀ i : ι, i ∈ c.support → l i = 1.

Thank you!

import data.finsupp.basic

open_locale big_operators classical

lemma sum_eq_sum {ι : Type*}
(l : ι → ℤ)
(c : ι →₀ ℕ) :
∑ (i : ι) in c.support, l i = ∑ (i : ι) in c.support, 1 :=
begin
end


#### Rémy Degenne (Feb 27 2021 at 12:21):

I did not test it, but it looks like it's what you need

#### Rémy Degenne (Feb 27 2021 at 12:23):

import data.finsupp.basic

open_locale big_operators classical

lemma sum_eq_sum {ι : Type*}
(l : ι → ℤ)
(c : ι →₀ ℕ) :
∑ (i : ι) in c.support, l i = ∑ (i : ι) in c.support, 1 :=
begin
refine finset.sum_congr rfl _,
-- ⊢ ∀ (x : ι), x ∈ c.support → l x = 1
end


#### Damiano Testa (Feb 27 2021 at 12:23):

Precisely, thanks! It also created a side goal asking me to prove that the two supports are equal!

Great!

#### Damiano Testa (Feb 27 2021 at 12:24):

I like the underscores!

#### Scott Morrison (Feb 27 2021 at 13:54):

There's in fact a tactic for this!

import data.finsupp.basic

open_locale big_operators classical

lemma sum_eq_sum {ι : Type*}
(l : ι → ℤ)
(c : ι →₀ ℕ)
(h : ∀ i ∈ c.support, l i = 1) :
∑ (i : ι) in c.support, l i = ∑ (i : ι) in c.support, 1 :=
begin
conv_lhs { apply_congr, skip, rw h x H, },
end


#### Damiano Testa (Feb 27 2021 at 13:58):

Ah, thanks! I can rarely get conv to work, since it either skips too much or gets stuck and does not move forward. In particular, I did not know the apply_congr command: inside conv I think that I only know congr, skip and rw

#### Kevin Buzzard (Feb 27 2021 at 13:59):

(sorry, my zulip didn't refresh for some reason)

Last updated: May 14 2021 at 03:27 UTC