constructor
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
case mp
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

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∀ (g h : G), ⁅g, h⁆ = 1) → ∀ (x : G), x ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆} ↔ x = 1