no goals
α : Type u_1
β : Type ?u.566270
γ : Type ?u.566273
δ : Type ?u.566276
ι : Type ?u.566279
R : Type ?u.566282
R' : Type ?u.566285
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ (Ι a b), P x) ↔
    (∀ᵐ (x : α) ∂Measure.restrict μ (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂Measure.restrict μ (Ioc b a), P x
rw [ae_restrict_uIoc_eq, eventually_sup]