no goals
α : Type u_1
β : Type ?u.708423
γ : Type ?u.708426
δ : Type ?u.708429
ι : Type ?u.708432
R : Type ?u.708435
R' : Type ?u.708438
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ ↑↑μ (sᶜ) = 0 ↔ ↑↑μ s = 1
rw [prob_compl_eq_one_sub hs, tsub_eq_zero_iff_le, one_le_prob_iff]