simp only [← zpowers_eq_closure, exists_prop]
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ closure {x} ↔ ∃ n < orderOf x, x ^ n = y
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ zpowers x ↔ ∃ n < orderOf x, x ^ n = y