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