no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s✝ t : Set α
ht : IsOpen t
s : Set α
⊢ closure s / t = s / t
simp_rw [div_eq_mul_inv, ht.inv.closure_mul]