no goals
α : Type u_1
β : Type ?u.367980
γ : Type ?u.367983
δ : Type ?u.367986
ι : Type ?u.367989
R : Type ?u.367992
R' : Type ?u.367995
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs : MeasurableSet s
⊢ ↑↑count s = ∑' (i : ↑s), 1
simp only [count, sum_apply, hs, dirac_apply', ← tsum_subtype s (1 : α → ℝ≥0∞), Pi.one_apply]