have hg: ∀ (x : ℕ),
    x ∈ Finset.range 101 → ∀ (y : ℕ), y ∈ Finset.range 101 → g x = g y → x = y := by
  intro a ha b hb hgab
  dsimp [g] at hgab
  have h5 : (a : ZMod 101) = (b : ZMod 101) := by linear_combination hgab
  have h8: a % 101 = b % 101 := Iff.mp (ZMod.natCast_eq_natCast_iff' a b 101) h5
  rw [Finset.mem_range] at ha hb
  rwa [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at h8
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∑ 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 = ∑ i ∈ Finset.range 101, f (y + ↑i)