no goals
α : Type u_1
β : Type ?u.145326
γ : Type ?u.145329
δ : Type ?u.145332
ι : Type ?u.145335
R : Type ?u.145338
R' : Type ?u.145341
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ ¬ν ≤ μ ↔ ∃ s, ↑↑μ s < ↑↑ν s
simp only [le_iff', not_forall, not_le]