no goals
α : Type u
β : Type v
X : Type ?u.217515
inst✝¹ : PseudoEMetricSpace α
x✝ y✝ z✝ : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r
simp [Prod.edist_eq]