no goals
α : Type u_1
β : Type ?u.905220
γ : Type ?u.905223
δ : Type ?u.905226
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂c • μ) = c * ∫⁻ (a : α), f a ∂μ
simp only [lintegral, iSup_subtype', SimpleFunc.lintegral_smul, ENNReal.mul_iSup, smul_eq_mul]