no goals
α : Type u_1
β : Type ?u.373940
γ : Type ?u.373943
δ : Type ?u.373946
ι : Type ?u.373949
R : Type ?u.373952
R' : Type ?u.373955
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Finite s
⊢ ↑↑count s = ↑(Finset.card (Finite.toFinset hs))
rw [← count_apply_finset, Finite.coe_toFinset]