case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ ↑↑(condCount s) (t ∪ u) = ↑↑(condCount s) t + ↑↑(condCount s) u
rw [condCount, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet,
  cond_apply _ hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]
no goals
case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)
exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]