simpa only [h, ciSup_const, Subgroup.mem_closure_singleton, one_zpow, exists_const] using h'
case mpr.mp
G : Type u_1
inst✝ : Group G
h : ∀ (g h : G), ⁅g, h⁆ = 1
g : G
h' : g ∈ ⨆ i, ⨆ i_1, Subgroup.closure {⁅i, i_1⁆}
⊢ 1 = g
no goals