rw [← Subgroup.zpowers_eq_closure]
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.closure {g}) = {x | ∃ i, g ^ i = x}
G : Type u_1
inst✝ : Group G
g : G
_h : ¬IsOfFinOrder g
⊢ ↑(Subgroup.zpowers g) = {x | ∃ i, g ^ i = x}