no goals
𝓕 : Type ?u.1214055
𝕜 : Type ?u.1214058
α : Type ?u.1214061
ι : Type ?u.1214064
κ : Type ?u.1214067
E : Type u_1
F : Type u_2
G : Type ?u.1214076
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f✝ g : α → E
f : E → F
hf : AntilipschitzWith K f
x y : E
⊢ ‖x / y‖ ≤ ↑K * ‖f x / f y‖
simp [← dist_eq_norm_div, hf.le_mul_dist x y]