simp only [coe_sum]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : CommMonoid β
I : Type u_4
f : I → SimpleFunc α ℝ
inst✝ : Fintype I
⊢ ↑(∑ i : I, f i) = ∑ i : I, ↑(f i)
no goals