Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
⊢ False
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ Nonempty Ω
by_contra maybe_empty
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : ↑↑↑μ univ = 0
⊢ False
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
⊢ False
have zero : (μ : Measure Ω) univ = 0 := by
  rw [univ_eq_empty_iff.mpr (not_nonempty_iff.mp maybe_empty), measure_empty]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : 1 = 0
⊢ False
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : ↑↑↑μ univ = 0
⊢ False
rw [measure_univ] at zero
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
zero : 1 = 0
⊢ False
exact zero_ne_one zero.symm
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
maybe_empty : ¬Nonempty Ω
⊢ ↑↑↑μ univ = 0
rw [univ_eq_empty_iff.mpr (not_nonempty_iff.mp maybe_empty), measure_empty]