specialize hx (n125 X) _
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∀ i ∈ {K | X ⊆ ↑K}, x ∈ ↑i
⊢ n125 X ∈ {K | X ⊆ ↑K}

case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : x ∈ ↑(n125 X)
⊢ ∃ x_1 ∈ n125Set X, List.prod x_1 = x