refine' ⟨[y], _, List.prod_singleton⟩
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ ∃ x ∈ n125Set X, List.prod x = y
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
y : G
hy : y ∈ X
⊢ [y] ∈ n125Set X