Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) (uᶜ) = ↑↑(condCount s) t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) (uᶜ) = ↑↑(condCount s) t
have : condCount s t = (condCount (s ∩ u) t * condCount (s ∩ u ∪ s ∩ uᶜ) (s ∩ u) +
    condCount (s ∩ uᶜ) t * condCount (s ∩ u ∪ s ∩ uᶜ) (s ∩ uᶜ)) := by
  rw [condCount_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
    (disjoint_compl_right.mono inf_le_right inf_le_right), Set.inter_union_compl]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) (uᶜ) =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) (uᶜ) = ↑↑(condCount s) t
rw [this]
no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) (uᶜ) =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
simp [condCount_inter_self hs]
no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
rw [condCount_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
  (disjoint_compl_right.mono inf_le_right inf_le_right), Set.inter_union_compl]