no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2568
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ K⁻¹ * nndist x y ≤ nndist (f x) (f y)
simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)