no goals
α : Type u
β : Type v
X : Type ?u.245069
ι : Type ?u.245072
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y₁ y₂ : β
⊢ dist (x, y₁) (x, y₂) = dist y₁ y₂
simp [Prod.dist_eq, dist_nonneg]