no goals
ι : Type u_2
ι' : Type ?u.3159831
α : ι → Type u_1
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ ↑↑(Measure.pi μ) (Metric.ball x r) = ∏ i : ι, ↑↑(μ i) (Metric.ball (x i) r)
rw [ball_pi _ hr, pi_pi]