no goals
α : Type u_1
β : Type ?u.369968
γ : Type ?u.369971
δ : Type ?u.369974
ι : Type ?u.369977
R : Type ?u.369980
R' : Type ?u.369983
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
s : Finset α
s_mble : MeasurableSet ↑s
⊢ ∑ i in s, 1 = ↑(Finset.card s)
simp