exact Subgroup.inv_mem _ (hi h1)
case a.intro.intro.cons.a.inr
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⁻¹
h1 : y_hd ∈ X⁻¹
⊢ y_hd⁻¹⁻¹ ∈ i
no goals