case inl
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑0 s)) s = mass 0 * (fun s => ENNReal.toNNReal (↑↑↑(normalize 0) s)) s

case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑(normalize μ) s)) s
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑(normalize μ) s)) s
obtain rfl | h := eq_or_ne μ 0
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : mass μ ≠ 0
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑(normalize μ) s)) s
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑(normalize μ) s)) s
have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff]
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : mass μ ≠ 0
⊢ ENNReal.toNNReal (↑↑↑μ s) =
    mass μ *
      ENNReal.toNNReal (↑↑↑{ val := ↑((mass μ)⁻¹ • μ), property := (_ : IsProbabilityMeasure ↑((mass μ)⁻¹ • μ)) } s)
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : mass μ ≠ 0
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑(normalize μ) s)) s
simp only [normalize, dif_neg mass_nonzero]
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : mass μ ≠ 0
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑((mass μ)⁻¹ • μ) s)) s
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : mass μ ≠ 0
⊢ ENNReal.toNNReal (↑↑↑μ s) =
    mass μ *
      ENNReal.toNNReal (↑↑↑{ val := ↑((mass μ)⁻¹ • μ), property := (_ : IsProbabilityMeasure ↑((mass μ)⁻¹ • μ)) } s)
change μ s = mass μ * ((mass μ)⁻¹ • μ) s
no goals
case inr
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
mass_nonzero : mass μ ≠ 0
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s = mass μ * (fun s => ENNReal.toNNReal (↑↑↑((mass μ)⁻¹ • μ) s)) s
simp only [toMeasure_smul, Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply,
  Measure.nnreal_smul_coe_apply, ne_eq, mass_zero_iff, ENNReal.toNNReal_mul, ENNReal.toNNReal_coe,
  mul_inv_cancel_left₀ mass_nonzero]
case inl
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ ENNReal.toNNReal (↑↑↑0 s) = 0
case inl
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ (fun s => ENNReal.toNNReal (↑↑↑0 s)) s = mass 0 * (fun s => ENNReal.toNNReal (↑↑↑(normalize 0) s)) s
simp only [zero_mass, coeFn_zero, Pi.zero_apply, MulZeroClass.zero_mul]
no goals
case inl
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
s : Set Ω
⊢ ENNReal.toNNReal (↑↑↑0 s) = 0
rfl
no goals
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ mass μ ≠ 0
rwa [μ.mass_nonzero_iff]