no goals
α : Type u_1
β : Type ?u.1027905
γ : Type ?u.1027908
δ : Type ?u.1027911
m : MeasurableSpace α
μ ν : Measure α
B : Set α
f : α → ℝ≥0∞
A : Set α
hB : MeasurableSet B
⊢ ((∫⁻ (x : α) in A ∩ B, f x ∂μ) + ∫⁻ (x : α) in A \ B, f x ∂μ) = ∫⁻ (x : α) in A, f x ∂μ
rw [← lintegral_add_measure, restrict_inter_add_diff _ hB]