Finset.sum_sub_distrib for `Nat`s

Stream: Is there code for X?

[Daniel Weber]

Do we have the following theorem?

import Mathlib

example {ι : Type*} (s : Finset ι) (f : ι → ℕ) (g : ι → ℕ) (hfg : g ≤ f) :
    ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x := by
  sorry

Note that this isn't docs#Finset.sum_sub_distrib because the naturals aren't a subtraction monoid

[Yaël Dillies]

It was already discussed before here. Maybe @Bhavik Mehta remembers

[Yaël Dillies]

Btw it would be called Finset.sum_tsub_distrib

[Bhavik Mehta]

Yaël Dillies said:

It was already discussed before here. Maybe Bhavik Mehta remembers

I have definitely wanted this at least twice before - found a version here: https://github.com/b-mehta/ExponentialRamsey/blob/7e17b629a915a082869f494c8afa56a3e1c7a88d/ExponentialRamsey/Prereq/Mathlib/Algebra/BigOperators/Ring.lean#L17 I'm pretty sure this worked on Lean 4 at the time, hopefully it's not too hard to adjust to current Lean 4. Something like this should _definitely_ be in mathlib. Feel free to upstream this file with credit!

[Daniel Weber]

#17130