no goals
𝓕 : Type u_1
𝕜 : Type ?u.369462
α : Type ?u.369465
ι : Type ?u.369468
κ : Type ?u.369471
E : Type u_2
F : Type u_3
G : Type ?u.369480
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖↑f x‖
x y : E
⊢ dist x y ≤ ↑K * dist (↑f x) (↑f y)
simpa only [dist_eq_norm_div, map_div] using h (x / y)