no goals
α : Type u_1
β : Type ?u.295789
γ : Type ?u.295792
δ : Type ?u.295795
ι : Type ?u.295798
R : Type ?u.295801
R' : Type ?u.295804
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ restrict μ (s ∪ t) + restrict μ (s ∩ t) = restrict μ s + restrict μ t
simpa only [union_comm, inter_comm, add_comm] using restrict_union_add_inter t hs