theorem MeasureTheory.Measure.integral_comp {α : Type u_1} {β : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : ProbabilityTheory.Kernel α β} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} (hf : Integrable f (μ.bind ⇑κ)) : ∫ (b : β), f b ∂μ.bind ⇑κ = ∫ (a : α), ∫ (b : β), f b ∂κ a ∂μ