no goals
α : Type u_1
β : Type ?u.76494
γ : Type ?u.76497
δ : Type ?u.76500
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ (∫⁻ (x : α), c ∂μ) < ⊤
simpa only [Measure.restrict_univ] using set_lintegral_const_lt_top (univ : Set α) hc