no goals
α : Type ?u.8596
G : Type u_1
A : Type ?u.8602
S : Type ?u.8605
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
⊢ closure s⁻¹ = closure s
simp only [← toSubmonoid_eq, closure_toSubmonoid, inv_inv, union_comm]