specialize h1 y_hd (List.mem_cons_self _ _)
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : ∀ x ∈ y_hd :: tail, x ∈ X ∪ X⁻¹
⊢ y_hd ∈ i
case a.intro.intro.cons.a
G : Type u_1
inst✝ : Group G
X : Set G
i : Subgroup G
hi : i ∈ {K | X ⊆ ↑K}
y_hd : G
tail : List G
y_ih : (∀ x ∈ tail, x ∈ X ∪ X⁻¹) → List.prod tail ∈ i
h1 : y_hd ∈ X ∪ X⁻¹
⊢ y_hd ∈ i