no goals
ι : Type ?u.5264
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f✝ : α → β
x✝ y✝ z : α
s : Set α
f : α → β
g : β → α
h : Isometry f
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y
rw [← h, hg _, hg _]