no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (s ∩ t) = ↑↑(condCount s) t
rw [condCount, cond_inter_self _ hs.measurableSet]