∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ f →
    Measurable f →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        Measurable g →
          (∀ t > 0, 0 ≤ g t) →
            ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
              ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)