sum_congr under modulo

Stream: mathlib4

[Yuval Filmus]

Suppose I know that f x = g x (mod m). How can I deduce that sum x, f x = sum x, g x (mod m)?
It is easy to prove this by induction, but does it already exist in mathlib?

[Aaron Liu]

You can pass to ZMod m

[Aaron Liu]

I also see docs#Finset.sum_int_mod and docs#Finset.sum_nat_mod, so you can rewrite your goal with those.