no goals
α : Type u
β : Type v
X : Type ?u.401932
ι : Type ?u.401935
inst✝³ : PseudoMetricSpace α
π : β → Type u_1
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
x : (b : β) → π b
r : ℝ
hr : r ≤ 0
⊢ ball x r = Set.pi Set.univ fun b => ball (x b) r
simp [ball_eq_empty.2 hr]