Rewriting under summation

Stream: new members

[Ching-Tsun Chou]

I have a sum of the following form:

∑ x ∈ s, (f x : ℕ)

where s is a Finset and the sum is embedded in a larger expression. I also have a lemma of the following form:

x ∈ s → f x = g x

I want to rewriting f x to g x in the sum in the larger expression. How do I do that?

[Ruben Van de Velde]

There's a lemma for that: docs#Finset.sum_congr

[Kyle Miller]

Potentially you can use simp_rw for the rewrite, since that congruence lemma is marked @[cong] so is known to simp

[Ruben Van de Velde]

... really?

[Kyle Miller]

Too bad, it doesn't seem to work here.

import Mathlib

example (f g : Nat → Nat) (s : Finset Nat) (h : ∀ x ∈ s, f x = g x) :
    ∑ x ∈ s, f x = ∑ x ∈ s, g x := by
  simp_rw [h]

In theory simp would handle this by using the additional hypothesis when discharging the side goal.

[Kyle Miller]

What do you know, +contextual did the trick:

import Mathlib

example (f g : Nat → Nat) (s : Finset Nat) (h : ∀ x ∈ s, f x = g x) :
    ∑ x ∈ s, f x = ∑ x ∈ s, g x := by
  simp_rw +contextual [h]

[Ching-Tsun Chou]

I was able to use Finset.sum_congr, but have not been able to get simp_rw to work.

[Kyle Miller]

(By the way, simp_rw here really is using Finset.sum_congr, and it's passing the membership proof to h. Just verified it with show_term, in case somehow +contextual enabled some other proof.)

[Ching-Tsun Chou]

(deleted)