no goals
𝓕 : Type u_1
𝕜 : Type ?u.408704
α : Type ?u.408707
ι : Type ?u.408710
κ : Type ?u.408713
E : Type u_2
F : Type u_3
G : Type ?u.408722
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 : AntilipschitzWith K ↑f
x : E
⊢ ‖x‖ ≤ ↑K * ‖↑f x‖
simpa only [dist_one_right, map_one] using h.le_mul_dist x 1