ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), a * f i) = ⨆ (i : ι), f i * a
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
rw [mul_comm, mul_iSup]
no goals
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), a * f i) = ⨆ (i : ι), f i * a
simp_rw [mul_comm]