no goals
α : Type u_1
β : Type ?u.373338
γ : Type ?u.373341
δ : Type ?u.373344
ι : Type ?u.373347
R : Type ?u.373350
R' : Type ?u.373353
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
s : Set α
s_fin : Set.Finite s
s_mble : MeasurableSet s
⊢ ↑↑count s = ↑(Finset.card (Finite.toFinset s_fin))
simp [←
  @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]
no goals
α : Type u_1
β : Type ?u.373338
γ : Type ?u.373341
δ : Type ?u.373344
ι : Type ?u.373347
R : Type ?u.373350
R' : Type ?u.373353
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
s : Set α
s_fin : Set.Finite s
s_mble : MeasurableSet s
⊢ MeasurableSet ↑(Finite.toFinset s_fin)
simpa only [Finite.coe_toFinset] using s_mble