have : ((Set.univ : Set ℕ).image fun i => g ^ i).Infinite := by
  simp
  apply Set.infinite_range_of_injective
  intro x y hxy
  rwa [pow_inj_iff_of_orderOf_eq_zero h] at hxy
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ Set.Infinite {x | ∃ i, g ^ i = x}