no goals
α : Type u_1
β : Type ?u.973547
γ : Type ?u.973550
δ : Type ?u.973553
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (0 < ∫⁻ (a : α), f a ∂μ) ↔ 0 < ↑↑μ (support f)
simp [pos_iff_ne_zero, hf, Filter.EventuallyEq, ae_iff, Function.support]