simp only [Set.mem_setOf]
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
hx : ∃ y, g ^ y = x
⊢ x ∈ {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)
x : G
hx : ∃ y, g ^ y = x
⊢ ∃ i, g ^ i = x