α : Type ?u.649
G : Type u_1
A : Type ?u.655
S✝ : Type ?u.658
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s⁻¹ ∈ closure S
α : Type ?u.649
G : Type u_1
A : Type ?u.655
S✝ : Type ?u.658
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)
rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
no goals
α : Type ?u.649
G : Type u_1
A : Type ?u.655
S✝ : Type ?u.658
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s⁻¹ ∈ closure S
exact subset_closure (mem_inv.mp hs)