case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ ∀ (s : Set Ω),
    MeasurableSet s →
      (fun s => ENNReal.toNNReal (↑↑↑(normalize (ProbabilityMeasure.toFiniteMeasure μ)) s)) s =
        (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ normalize (ProbabilityMeasure.toFiniteMeasure μ) = μ
apply ProbabilityMeasure.eq_of_forall_apply_eq
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ (fun s => ENNReal.toNNReal (↑↑↑(normalize (ProbabilityMeasure.toFiniteMeasure μ)) s)) s =
    (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ ∀ (s : Set Ω),
    MeasurableSet s →
      (fun s => ENNReal.toNNReal (↑↑↑(normalize (ProbabilityMeasure.toFiniteMeasure μ)) s)) s =
        (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
intro s _s_mble
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ (mass (ProbabilityMeasure.toFiniteMeasure μ))⁻¹ *
      (fun s => ENNReal.toNNReal (↑↑↑(ProbabilityMeasure.toFiniteMeasure μ) s)) s =
    (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ (fun s => ENNReal.toNNReal (↑↑↑(normalize (ProbabilityMeasure.toFiniteMeasure μ)) s)) s =
    (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
rw [μ.toFiniteMeasure.normalize_eq_of_nonzero μ.toFiniteMeasure_nonzero s]
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ ENNReal.toNNReal (↑↑↑(ProbabilityMeasure.toFiniteMeasure μ) s) = ENNReal.toNNReal (↑↑↑μ s)
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ (mass (ProbabilityMeasure.toFiniteMeasure μ))⁻¹ *
      (fun s => ENNReal.toNNReal (↑↑↑(ProbabilityMeasure.toFiniteMeasure μ) s)) s =
    (fun s => ENNReal.toNNReal (↑↑↑μ s)) s
simp only [ProbabilityMeasure.mass_toFiniteMeasure, inv_one, one_mul]
no goals
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0✝ : MeasurableSpace Ω
μ✝ : FiniteMeasure Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ ENNReal.toNNReal (↑↑↑(ProbabilityMeasure.toFiniteMeasure μ) s) = ENNReal.toNNReal (↑↑↑μ s)
congr