no goals
M : Type u_1
N : Type ?u.361198
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
hS : IsClosed ↑S
m : M
h : ‖↑(mk' S) m‖ = 0
⊢ m ∈ S
rwa [quotient_norm_eq_zero_iff, hS.closure_eq] at h