rw [Finset.eq_univ_iff_forall]
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
⊢ Finset.image g (Finset.range 101) = Finset.univ
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
⊢ ∀ (x : ZMod 101), x ∈ Finset.image g (Finset.range 101)