no goals
ι : Type u_1
ι' : Type ?u.3159203
α : ι → Type u_2
inst✝² : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ ↑↑(Measure.pi μ) univ = ∏ i : ι, ↑↑(μ i) univ
rw [← pi_univ, pi_pi μ]