no goals
α : Type u_1
β : Type ?u.595108
γ : Type ?u.595111
δ : Type ?u.595114
ι : Type ?u.595117
R : Type ?u.595120
R' : Type ?u.595123
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : PartialOrder α
a b : α
ha : ↑↑μ {a} = 0
⊢ Iio a =ᶠ[ae μ] Iic a
rw [← Iic_diff_right, diff_ae_eq_self, measure_mono_null (Set.inter_subset_right _ _) ha]