Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑(condCount {ω}) t = if ω ∈ t then 1 else 0
rw [condCount, cond_apply _ (measurableSet_singleton ω), Measure.count_singleton, inv_one,
  one_mul]
case inl
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 1

case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 0
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0
split_ifs
no goals
case inl
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 1
rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]
no goals
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ {ω} ∩ t = {ω}
simpa
no goals
case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 0
rw [(by simpa : ({ω} : Set Ω) ∩ t = ∅), Measure.count_empty]
no goals
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ {ω} ∩ t = ∅
simpa