no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u t : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) t + ↑↑(condCount s) (tᶜ) = 1
rw [← condCount_union hs disjoint_compl_right, Set.union_compl_self,
  (condCount_isProbabilityMeasure hs hs').measure_univ]