no goals
α : Type u_1
β : Type ?u.971808
γ : Type ?u.971811
δ : Type ?u.971814
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (x : α), 0 ∂μ) ≠ ⊤
simp [lintegral_zero, zero_ne_top]