Restricted Congr

Stream: new members

[Emma R. Hasson]

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]

Is docs#finset.sum_congr helpful?

[Eric Wieser]

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

[Emma R. Hasson]

That works! Thanks.