no goals
α : Type u_1
β : Type ?u.297875
γ : Type ?u.297878
δ : Type ?u.297881
ι : Type ?u.297884
R : Type ?u.297887
R' : Type ?u.297890
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : Disjoint s t
hs : MeasurableSet s
⊢ restrict μ (s ∪ t) = restrict μ s + restrict μ t
rw [union_comm, restrict_union h.symm hs, add_comm]