simp only [hy, n125Set, forall_eq, true_or_iff, Set.mem_setOf, List.mem_singleton,
  Set.mem_union]
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
no goals