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