intro x y hxy
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Function.Injective fun i => g ^ i
case hi
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
x y : ℕ
hxy : (fun i => g ^ i) x = (fun i => g ^ i) y
⊢ x = y