no goals
α : Type u_1
β : Type ?u.565282
γ : Type ?u.565285
δ : Type ?u.565288
ι : Type ?u.565291
R : Type ?u.565294
R' : Type ?u.565297
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : LinearOrder α
a b : α
⊢ ae (Measure.restrict μ (Ι a b)) = ae (Measure.restrict μ (Ioc a b)) ⊔ ae (Measure.restrict μ (Ioc b a))
simp only [uIoc_eq_union, ae_restrict_union_eq]