Theorem: SimpleFunc.coe_sum' (RandomGraphs/simple_func.lean)

State before:
ι : 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)
Tactic:
simp only [coe_sum]
State after:
no goals