no goals
α : Type u_1
β : Type ?u.369064
γ : Type ?u.369067
δ : Type ?u.369070
ι : Type ?u.369073
R : Type ?u.369076
R' : Type ?u.369079
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
⊢ ↑↑count ∅ = 0
rw [count_apply MeasurableSet.empty, tsum_empty]