no goals
ι : Type ?u.19593
α : Type u_1
β : Type ?u.19599
γ : Type ?u.19602
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t
hd : AEDisjoint μ s t
⊢ ↑↑μ (s ∪ t) = ↑↑μ s + ↑↑μ t
rw [← measure_union_add_inter₀ s ht, hd, add_zero]