Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count s / ↑↑Measure.count Set.univ = ↑↑Measure.count s / ↑(Fintype.card Ω)
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑(condCount Set.univ) s = ↑↑Measure.count s / ↑(Fintype.card Ω)
rw [condCount, cond_apply _ MeasurableSet.univ, ← ENNReal.div_eq_inv_mul, Set.univ_inter]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count Set.univ = ↑(Fintype.card Ω)
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count s / ↑↑Measure.count Set.univ = ↑↑Measure.count s / ↑(Fintype.card Ω)
congr
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ (Finset.sum Finset.univ fun x => 1) = ↑(Fintype.card Ω)

case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ MeasurableSet ↑Finset.univ
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count Set.univ = ↑(Fintype.card Ω)
rw [← Finset.coe_univ, Measure.count_apply, Finset.univ.tsum_subtype' fun _ => (1 : ENNReal)]
no goals
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ (Finset.sum Finset.univ fun x => 1) = ↑(Fintype.card Ω)
simp [Finset.card_univ]
no goals
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ MeasurableSet ↑Finset.univ
exact (@Finset.coe_univ Ω _).symm ▸ MeasurableSet.univ