no goals
𝓕 : Type u_1
𝕜 : Type ?u.145958
α : Type ?u.145961
ι : Type ?u.145964
κ : Type ?u.145967
E : Type u_2
F : Type u_3
G : Type ?u.145976
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 : 𝓕
C : ℝ
h : ∀ (x : E), ‖↑f x‖ ≤ C * ‖x‖
x y : E
⊢ dist (↑f x) (↑f y) ≤ C * dist x y
simpa only [dist_eq_norm_div, map_div] using h (x / y)