simp only [SetLike.mem_coe, Set.mem_singleton_iff, Set.setOf_exists, Subgroup.closure_iUnion,
  Set.setOf_eq_eq_singleton']
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
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1) ↔ ∀ (g h : G), ⁅g, h⁆ = 1