no goals
ι : Type ?u.147412
α : Type ?u.147415
X : Type ?u.147418
M : Type u_1
N : Type ?u.147424
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
s : Submonoid M
⊢ ↑(topologicalClosure s) = _root_.closure ↑s
rfl