rw [Finset.mem_range] at ha hb
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a ∈ Finset.range 101
b : ℕ
hb : b ∈ Finset.range 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
a : ℕ
ha : a < 101
b : ℕ
hb : b < 101
hgab : y + ↑a = y + ↑b
h5 : ↑a = ↑b
h8 : a % 101 = b % 101
⊢ a = b