ext
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
⊢ ↑(Subgroup.closure {g}) = {x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x}
case h
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x}