no goals
α : Type u_1
β : Type ?u.1028581
γ : Type ?u.1028584
δ : Type ?u.1028587
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
A : Set α
hA : MeasurableSet A
⊢ ((∫⁻ (x : α) in A, f x ∂μ) + ∫⁻ (x : α) in Aᶜ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
rw [← lintegral_add_measure, Measure.restrict_add_restrict_compl hA]