no goals
α : Type u_1
β : Type ?u.294414
γ : Type ?u.294417
δ : Type ?u.294420
ι : Type ?u.294423
R : Type ?u.294426
R' : Type ?u.294429
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
ht : NullMeasurableSet t
⊢ restrict μ (s ∪ t) + restrict μ (s ∩ t) = restrict μ s + restrict μ t
rw [← restrict_inter_add_diff₀ (s ∪ t) ht, union_inter_cancel_right, union_diff_right, ←
  restrict_inter_add_diff₀ s ht, add_comm, ← add_assoc, add_right_comm]