case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t

case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
by_cases hst : s ∩ t = ∅
case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ 0

case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ ⊤
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
rw [condCount, condCount, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet,
  cond_apply _ (hs.inter_of_left _).measurableSet, mul_comm _ (Measure.count (s ∩ t)),
  ← mul_assoc, mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc, ENNReal.mul_inv_cancel, one_mul,
  mul_comm, Set.inter_assoc]
no goals
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
rw [hst, condCount_empty_meas, Measure.coe_zero, Pi.zero_apply, MulZeroClass.zero_mul,
  condCount_eq_zero_iff hs, ← Set.inter_assoc, hst, Set.empty_inter]
no goals
case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ 0
rwa [← Measure.count_eq_zero_iff] at hst
no goals
case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ ⊤
exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne