no goals
α : Type u_1
β : Type ?u.1762622
γ : Type ?u.1762625
δ : Type ?u.1762628
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : (∫⁻ (a : α), f a ∂μ) ≠ ⊤
⊢ ↑↑(withDensity μ f) univ < ⊤
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, lt_top_iff_ne_top]