no goals
α : Type u
β : Type v
X : Type ?u.247136
ι : Type ?u.247139
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r
simp [Prod.dist_eq]