Zulip Chat Archive

Stream: new members

Topic: bsum ext


view this post on Zulip 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
  admit,
end

view this post on Zulip Rémy Degenne (Feb 27 2021 at 12:21):

docs#finset.sum_congr ?

view this post on Zulip Rémy Degenne (Feb 27 2021 at 12:21):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Feb 27 2021 at 12:24):

I like the underscores!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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