no goals
α : Type u_1
β : Type ?u.298586
γ : Type ?u.298589
δ : Type ?u.298592
ι : Type ?u.298595
R : Type ?u.298598
R' : Type ?u.298601
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : MeasurableSet s
⊢ restrict μ s + restrict μ (sᶜ) = μ
rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,
  restrict_univ]