no goals
ι : Type ?u.20428
α : Type u_1
β : Type ?u.20434
γ : Type ?u.20437
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]