no goals
α : Type u_1
β : Type ?u.3445
E : Type u_2
F : Type ?u.3451
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hst : AEDisjoint μ s t
ht : NullMeasurableSet t
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ (∫ (x : α) in s ∪ t, f x ∂μ) = (∫ (x : α) in s, f x ∂μ) + ∫ (x : α) in t, f x ∂μ
simp only [IntegrableOn, Measure.restrict_union₀ hst ht, integral_add_measure hfs hft]