simp_rw [← n1_2_26_ii']
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
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⁆ = 1