∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f →
    ∀ {i : δ}, i ∉ s → ∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, fun x => ∫⁻ (xᵢ : X i), f (Function.update x i xᵢ) ∂μ i ∂μ