M : Type u_1
N : Type ?u.113147
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ (⨅ (y : ↑↑S), dist (-m) ↑y) = ⨅ (a : ↑↑S), ‖m + ↑a‖
M : Type u_1
N : Type ?u.113147
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg,
  neg_coe_set (H := S), infDist_eq_iInf]
no goals
M : Type u_1
N : Type ?u.113147
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ (⨅ (y : ↑↑S), dist (-m) ↑y) = ⨅ (a : ↑↑S), ‖m + ↑a‖
simp only [dist_eq_norm', sub_neg_eq_add, add_comm]