simp only [Set.mem_iInter, SetLike.mem_coe]
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ x ∈ ⋂ s ∈ {K | X ⊆ ↑K}, ↑s
case a
G : Type u_1
inst✝ : Group G
X : Set G
x : G
hx : ∃ x_1, (∀ x ∈ x_1, x ∈ X ∪ X⁻¹) ∧ List.prod x_1 = x
⊢ ∀ i ∈ {K | X ⊆ ↑K}, x ∈ i