∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [inst : DecidableEq ι] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {s : Finset ι} {f : ((i : ι) → X i) → E},
  MeasureTheory.StronglyMeasurable f →
    ∀ (x : (i : ι) → X i),
      ∫ (y : (i : ι) → X i), f y ∂MeasureTheory.Measure.infinitePi μ =
        ∫ (y : (i : ↥s) → X ↑i), f (Function.updateFinset x s y) ∂MeasureTheory.Measure.pi fun i => μ ↑i