Theorem: l1_2_15_ii (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
g : G
⊢ ↑(Subgroup.closure {g}) = {x | ∃ k, g ^ k = x}
Tactic:
ext
State after:
case h
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ k, g ^ k = x}

State before:
case h
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ ↑(Subgroup.closure {g}) ↔ x✝ ∈ {x | ∃ k, g ^ k = x}
Tactic:
simp only [SetLike.mem_coe, Set.mem_setOf_eq, Subgroup.mem_closure_singleton]
State after:
no goals