bsum ext

Stream: new members

[Damiano Testa]

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
  admit,
end

[Rémy Degenne]

docs#finset.sum_congr ?

[Rémy Degenne]

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

[Rémy Degenne]

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]

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

Great!

[Damiano Testa]

I like the underscores!

[Scott Morrison]

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]

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]

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