no goals
α : Type u_1
β : Type ?u.296515
γ : Type ?u.296518
δ : Type ?u.296521
ι : Type ?u.296524
R : Type ?u.296527
R' : Type ?u.296530
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : AEDisjoint μ s t
ht : NullMeasurableSet t
⊢ restrict μ (s ∪ t) = restrict μ s + restrict μ t
simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]