no goals
α : Type u_1
β : Type ?u.945819
γ : Type ?u.945822
δ : Type ?u.945825
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ
simp_rw [mul_comm, lintegral_const_mul_le r f]