no goals
ι : Type ?u.1422
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
h : Isometry f
x y : α
⊢ edist x y ≤ ↑1 * edist (f x) (f y)
simp only [h x y, ENNReal.coe_one, one_mul, le_refl]