no goals
α : Type u_1
β : Type ?u.1027026
γ : Type ?u.1027029
δ : Type ?u.1027032
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
A B : Set α
hB : MeasurableSet B
hAB : Disjoint A B
⊢ (∫⁻ (a : α) in A ∪ B, f a ∂μ) = (∫⁻ (a : α) in A, f a ∂μ) + ∫⁻ (a : α) in B, f a ∂μ
rw [restrict_union hAB hB, lintegral_add_measure]