no goals
α : Type u_2
β✝ : Type ?u.947084
γ : Type ?u.947087
δ : Type ?u.947090
m : MeasurableSpace α
μ ν✝ : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
⊢ (∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ) = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
simp [lintegral_const_mul'' _ hg, lintegral_mul_const'' _ hf]