no goals
α : Type u_2
α' : Type ?u.4447223
β : Type u_1
β' : Type ?u.4447229
γ : Type ?u.4447232
E : Type ?u.4447235
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ ↑↑(Measure.prod μ ν) s = 0 ↔ (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0
rw [prod_apply hs, lintegral_eq_zero_iff (measurable_measure_prod_mk_left hs)]