rw[← Finset.sum_image hg]
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ i ∈ Finset.range 101, f (y + ↑i)
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
⊢ ∑ z : ZMod 101, f z = ∑ x ∈ Finset.image (fun x => g x) (Finset.range 101), f x