no goals
α : Type u_1
β : Type ?u.298946
γ : Type ?u.298949
δ : Type ?u.298952
ι : Type ?u.298955
R : Type ?u.298958
R' : Type ?u.298961
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : MeasurableSet s
⊢ restrict μ (sᶜ) + restrict μ s = μ
rw [add_comm, restrict_add_restrict_compl hs]