no goals
α : Type u_1
β : Type ?u.33444
E : Type u_2
F : Type ?u.33450
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : NullMeasurableSet s
hfi : Integrable f
⊢ ((∫ (x : α) in s, f x ∂μ) + ∫ (x : α) in sᶜ, f x ∂μ) = ∫ (x : α), f x ∂μ
rw [← integral_union_ae (@disjoint_compl_right (Set α) _ _).aedisjoint hs.compl hfi.integrableOn
    hfi.integrableOn,
  union_compl_self, integral_univ]