no goals
α : Type u_2
β : Type ?u.256888
γ : Type ?u.256891
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
R : Type u_1
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
a : R
⊢ (∑' (i : α), a • f i) = a • ∑' (i : α), f i
simpa only [smul_one_mul] using @ENNReal.tsum_mul_left _ (a • (1 : ℝ≥0∞)) _