rw [Set.ext_iff]
G : Type u_1
inst✝ : Group G
⊢ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) = {1} ↔ ∀ (g h : G), g * h = h * g
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ↑(Subgroup.closure {x | ∃ g h, ⁅g, h⁆ = x}) ↔ x ∈ {1}) ↔ ∀ (g h : G), g * h = h * g