no goals
V : Type ?u.211727
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.211736
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
K : ℝ≥0
h : ∀ (x : V₁), ‖x‖ ≤ ↑K * ‖↑f x‖
x y : V₁
⊢ dist x y ≤ ↑K * dist (↑f x) (↑f y)
simpa only [dist_eq_norm, map_sub] using h (x - y)