no goals
M : Type u_1
N : Type ?u.464490
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(AddSubgroup.normedMk S) m‖ = sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker (AddSubgroup.normedMk S)))
simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m