Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ProbabilityMeasure.toFiniteMeasure (normalize μ) =
    (mass μ)⁻¹ • mass μ • ProbabilityMeasure.toFiniteMeasure (normalize μ)
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ProbabilityMeasure.toFiniteMeasure (normalize μ) = (mass μ)⁻¹ • μ
nth_rw 3 [μ.self_eq_mass_smul_normalize]
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ProbabilityMeasure.toFiniteMeasure (normalize μ) =
    ((mass μ)⁻¹ • mass μ) • ProbabilityMeasure.toFiniteMeasure (normalize μ)
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ProbabilityMeasure.toFiniteMeasure (normalize μ) =
    (mass μ)⁻¹ • mass μ • ProbabilityMeasure.toFiniteMeasure (normalize μ)
rw [← smul_assoc]
no goals
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ProbabilityMeasure.toFiniteMeasure (normalize μ) =
    ((mass μ)⁻¹ • mass μ) • ProbabilityMeasure.toFiniteMeasure (normalize μ)
simp only [μ.mass_nonzero_iff.mpr nonzero, Algebra.id.smul_eq_mul, inv_mul_cancel, Ne.def,
  not_false_iff, one_smul]