rw [← orderOf_eq_zero_iff] at h
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite {x | ∃ i, g ^ i = x}
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
⊢ Set.Infinite {x | ∃ i, g ^ i = x}