no goals
α : Type u_1
β : Type ?u.255728
γ : Type ?u.255731
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
⊢ (∑' (i : α), f i * a) = (∑' (i : α), f i) * a
simp [mul_comm, ENNReal.tsum_mul_left]