no goals
α : Type u_1
β : Type ?u.586
γ : Type ?u.589
δ : Type ?u.592
ι : Type ?u.595
R : Type ?u.598
R' : Type ?u.601
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ᵐ (x : α) ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Ioc b a → P x
simp only [uIoc_eq_union, mem_union, or_imp, eventually_and]