no goals
M : Type u_1
N : Type ?u.25731
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ ‖x‖ = infDist 0 {m | ↑m = x}
simp only [AddSubgroup.quotient_norm_eq, infDist_eq_iInf, sInf_image', dist_zero_left]