no goals
α : Type u_1
β : Type ?u.144465
γ : Type ?u.144468
δ : Type ?u.144471
ι : Type ?u.144474
R : Type ?u.144477
R' : Type ?u.144480
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ ¬ν ≤ μ ↔ ∃ s, MeasurableSet s ∧ ↑↑μ s < ↑↑ν s
simp only [le_iff, not_forall, not_le, exists_prop]