no goals
α : Type u_1
β : Type ?u.652108
γ : Type ?u.652111
δ : Type ?u.652114
ι : Type ?u.652117
R : Type ?u.652120
R' : Type ?u.652123
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ ¬↑↑μ univ = 0
simp [measure_univ]