∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [inst_3 : Fintype δ] (s : Finset δ)
  {f g : ((i : δ) → X i) → ENNReal},
  Measurable f →
    Measurable g →
      ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ →
        ∫⁻ (x : (i : δ) → X i), f x ∂MeasureTheory.Measure.pi μ =
          ∫⁻ (x : (i : δ) → X i), g x ∂MeasureTheory.Measure.pi μ