no goals
α : Type u_3
α' : Type ?u.2386685
β : Type u_1
β' : Type ?u.2386691
γ : Type ?u.2386694
E : Type u_2
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α × β → E
hf : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (fun x => ∫ (y : β), f (x, y) ∂ν) =ᶠ[ae μ] fun x => ∫ (y : β), AEStronglyMeasurable.mk f hf (x, y) ∂ν
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx