∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ (t : Set ↑s) (f : α → ENNReal),
      ∫⁻ (x : ↑s) in t, f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ