Zulip Chat Archive

Stream: new members

Topic: Restricted Congr


Emma R. Hasson (Jul 05 2022 at 19:54):

What is the correct tactic to use here? Congr doesn't seem to catch the fact that it is only true for x ∈ s.

example (f g :   ) (s : finset ) (hs :  x  s, f x = g x) :
   x in s, f x =  x in s, g x :=
begin
  congr' with x,
  -- not true for all x, only true for x ∈ s
end

Damiano Testa (Jul 05 2022 at 19:58):

Is docs#finset.sum_congr helpful?

Eric Wieser (Jul 05 2022 at 19:59):

I think the proof is finset.sum_congr rfl hs, so yes!

Emma R. Hasson (Jul 05 2022 at 20:06):

That works! Thanks.


Last updated: Dec 20 2023 at 11:08 UTC