case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ 0

case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ ⊤
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) Set.univ = 1
rw [condCount, cond_apply _ hs.measurableSet, Set.inter_univ, ENNReal.inv_mul_cancel]
no goals
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ 0
exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
no goals
case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ ⊤
exact (Measure.count_apply_lt_top.2 hs).ne