case h
G : Type u_1
inst✝² : Group G
A : Type ?u.4059
inst✝¹ : AddGroup A
N : Type ?u.4065
inst✝ : Group N
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}
G : Type u_1
inst✝² : Group G
A : Type ?u.4059
inst✝¹ : AddGroup A
N : Type ?u.4065
inst✝ : Group N
g : G
⊢ zpowers g = closure {g}
ext
no goals
case h
G : Type u_1
inst✝² : Group G
A : Type ?u.4059
inst✝¹ : AddGroup A
N : Type ?u.4065
inst✝ : Group N
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}
exact mem_closure_singleton.symm