no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y
x y : α
⊢ edist (f x) (f y) ≤ ↑1 * edist x y
simp only [ENNReal.coe_one, one_mul, h]