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