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
rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
  inv_inv]