intro a ha b hb hgab
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
⊢ ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
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 : g a = g b
⊢ a = b