apply Set.Infinite.mono _ this
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}
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
⊢ (fun i => g ^ i) '' Set.univ ⊆ {x | ∃ i, g ^ i = x}