no goals
ι : Type ?u.9758
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
z : E
hs : Convex ℝ s
⊢ ConvexOn ℝ s fun z' => dist z' z
simpa [dist_eq_norm, preimage_preimage] using
  (convexOn_norm (hs.translate (-z))).comp_affineMap (AffineMap.id ℝ E - AffineMap.const ℝ E z)