no goals
ι : Type ?u.2341
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f✝ : α → β
x✝ y✝ z : α
s : Set α
δ : Type u_1
inst✝ : PseudoEMetricSpace δ
f : α → β
g : γ → δ
hf : Isometry f
hg : Isometry g
x y : α × γ
⊢ edist (Prod.map f g x) (Prod.map f g y) = edist x y
simp only [Prod.edist_eq, hf.edist_eq, hg.edist_eq, Prod_map]