obtain ⟨y, h1, rfl⟩ := hx
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 : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
⊢ x ∈ i
case a.intro.intro
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y : List G
h1 : ∀ x ∈ y, x ∈ X ∪ X⁻¹
⊢ List.prod y ∈ i