no goals
α✝ : Type ?u.4019
β✝ : Type ?u.4022
γ : Type ?u.4025
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y
simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y