no goals
α : Type u_1
β : Type ?u.6535
γ : Type ?u.6538
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
⊢ edist x y ≤ ↑1 * edist (id x) (id y)
simp only [ENNReal.coe_one, one_mul, id, le_refl]