no goals
α : Type u_1
α' : Type ?u.5367515
β : Type u_2
β' : Type ?u.5367521
γ : Type ?u.5367524
E : Type ?u.5367527
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
⊢ (∫⁻ (z : α × β), f z.fst * g z.snd ∂Measure.prod μ ν) = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
simp [lintegral_prod _ (hf.fst.mul hg.snd), lintegral_lintegral_mul hf hg]