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