no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3257
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ ↑K⁻¹ * dist x y ≤ dist (f x) (f y)
exact_mod_cast hf.mul_le_nndist x y