MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul'

theorem lintegral_comp_eq_lintegral_distribution_mul' (μ : Measure α)    (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g) :    ∫⁻ ω, (∫⁻ t in (Iio (f ω)), g t) ∂μ =      ∫⁻ t, distribution f t μ * g t := by  rcases f_mble with ⟨fF, hF, f_eq_F⟩  convert lintegral_comp_eq_lintegral_distribution_mul μ hF g_mble using 1  · apply lintegral_congr_ae    filter_upwards [f_eq_F] with ω hω    congr  · congr with t    congr 1    apply distribution_congr_ae f_eq_F