no goals
α : Type u_1
β : Type ?u.555132
γ : Type ?u.555135
δ : Type ?u.555138
ι : Type ?u.555141
R : Type ?u.555144
R' : Type ?u.555147
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ s t : Set α
⊢ ae (Measure.restrict μ (s ∪ t)) = ae (Measure.restrict μ s) ⊔ ae (Measure.restrict μ t)
simp [union_eq_iUnion, iSup_bool_eq]