no goals
α : Type u_1
β : Type ?u.1772355
γ : Type ?u.1772358
δ : Type ?u.1772361
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h : withDensity μ f = 0
⊢ f =ᶠ[ae μ] 0
rw [← lintegral_eq_zero_iff' hf, ← set_lintegral_univ, ← withDensity_apply _ MeasurableSet.univ,
  h, Measure.coe_zero, Pi.zero_apply]