no goals
α : Type ?u.141598
G✝ : Type ?u.141601
M : Type ?u.141604
R : Type ?u.141607
A : Type ?u.141610
inst✝² : Monoid M
inst✝¹ : AddMonoid A
G : Type u_1
inst✝ : Group G
S : Set G
x : G
⊢ x ∈ closure S⁻¹ ↔ x⁻¹ ∈ closure S
rw [closure_inv, mem_inv]