no goals
ι : Type u_2
ι' : Type ?u.1293941
α : ι → Type u_1
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
hs : Set.Nonempty (Set.pi univ s)
⊢ piPremeasure m (Set.pi univ s) = ∏ i : ι, ↑(m i) (s i)
simp [hs, piPremeasure]