no goals
α : Type u_1
β : Type ?u.707839
γ : Type ?u.707842
δ : Type ?u.707845
ι : Type ?u.707848
R : Type ?u.707851
R' : Type ?u.707854
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ ↑↑μ (sᶜ) = 1 - ↑↑μ s
simpa only [measure_univ] using measure_compl hs (measure_lt_top μ s).ne