MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul

theorem lintegral_comp_eq_lintegral_distribution_mul (μ : Measure α)    (f_mble : Measurable f) (g_mble : AEMeasurable g) :    ∫⁻ ω, (∫⁻ t in (Iio (f ω)), g t) ∂μ =      ∫⁻ t, distribution f t μ * g t := by  revert f  apply Measurable.ennreal_induction'  · apply SimpleFunc.induction    · intro c s hs      simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,        SimpleFunc.coe_zero, piecewise_eq_indicator]      simp_rw [distribution_indicator_const, ← indicator_mul_left]      rw [lintegral_indicator measurableSet_Iio, enorm_eq_self,        lintegral_const_mul'' _ g_mble.restrict]      calc _        _ = ∫⁻ (ω : α) in s, (∫⁻ (t : ℝ≥0∞) in Iio c, g t) ∂μ := by          rw [← lintegral_indicator hs]          congr with ω          unfold indicator          split_ifs with hω          · simp          · simp      rw [lintegral_const, mul_comm]      simp    · intro f F disjoint hf hF      simp only [SimpleFunc.coe_add, Pi.add_apply]      calc _        _ = ∫⁻ (ω : α), (∫⁻ t in Iio (f ω), g t) + (∫⁻ t in Iio (F ω), g t) ∂μ := by          congr with ω          by_cases hω : ω ∉ Function.support f          · simp only [Function.mem_support, ne_eq, Decidable.not_not] at hω            rw [hω]            simp          by_cases hω' : ω ∉ Function.support F          · simp only [Function.mem_support, ne_eq, Decidable.not_not] at hω'            rw [hω']            simp          contrapose! disjoint          rw [@not_disjoint_iff]          push Not at hω hω'          use ω        _ = ∫⁻ (t : ℝ≥0∞), (distribution (⇑f) t μ + distribution (⇑F) t μ) * g t := by          simp_rw [add_mul]          rw [lintegral_add_left, lintegral_add_left' (by fun_prop)]          · congr          --TODO: maybe this can be done by fun_prop once `SimpleFunc.measurable_comp'` is tagged?          apply SimpleFunc.measurable_comp' (g := fun y ↦ ∫⁻ (t : ℝ≥0∞) in Iio y, g t)        _ = ∫⁻ (t : ℝ≥0∞), distribution (⇑f + ⇑F) t μ * g t := by          congr with t          congr          rw [distribution_add disjoint (by fun_prop)]  · intro fs hfs h    have {ω : α} : ∫⁻ (t : ℝ≥0∞) in Iio ((fun x ↦ ⨆ n, (fs n) x) ω), g t =        ⨆ n, ∫⁻ (t : ℝ≥0∞) in Iio ((fs n) ω), g t := by      rw [← iUnion_Iio_eq_Iio_iSup, setLIntegral_iUnion_of_directed]      intro n m      use max n m      simp only [Iio_subset_Iio_iff]      constructor      · apply hfs        exact le_max_left n m      · apply hfs        exact le_max_right n m    simp_rw [this]    have {t : ℝ≥0∞} : distribution (fun a ↦ (⨆ n, fs n a)) t μ * g t = ⨆ n, distribution (fs n) t μ * g t := by      rw [← ENNReal.iSup_mul]      congr      unfold distribution      simp only [enorm_eq_self]      rw [← Directed.measure_iUnion]      · congr 1        ext ω        rw [mem_iUnion, mem_setOf_eq, lt_iSup_iff]        rfl      · intro n m        use max n m        simp only [setOf_subset_setOf]        constructor <;>        · intro ω hω          apply hω.trans_le (hfs _ _)          simp    simp_rw [this]    rw [lintegral_iSup', lintegral_iSup']    · congr with n      exact h n    · intro n      fun_prop    · filter_upwards [] with t      intro n m hmn      dsimp only      gcongr      filter_upwards [] with ω      simp only [enorm_eq_self]      apply hfs hmn    · intro n      --TODO: maybe this can be done by fun_prop once `SimpleFunc.measurable_comp'` is tagged?      apply Measurable.aemeasurable      apply SimpleFunc.measurable_comp' (g := fun y ↦ ∫⁻ (t : ℝ≥0∞) in Iio y, g t)    · filter_upwards [] with t      intro n m hmn      dsimp only      gcongr      apply hfs hmn