no goals
α : Type u_1
β : Type ?u.343849
γ : Type ?u.343852
δ : Type ?u.343855
ι : Type ?u.343858
R : Type ?u.343861
R' : Type ?u.343864
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : Bool → Measure α
⊢ sum f = f true + f false
rw [sum_fintype, Fintype.sum_bool]