no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ↑((fun s => ENNReal.toNNReal (↑↑↑ν s)) s) = ↑↑↑ν s
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
  toMeasure_comp_toFiniteMeasure_eq_toMeasure]