no goals
α : Type u_1
β : Type ?u.944622
γ : Type ?u.944625
δ : Type ?u.944628
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), f a * r ∂μ) = (∫⁻ (a : α), f a ∂μ) * r
simp_rw [mul_comm, lintegral_const_mul r hf]