no goals
α : Type u_1
β : Type ?u.49654
E : Type u_2
F : Type ?u.49660
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s
hg : IntegrableOn g (sᶜ)
⊢ (∫ (x : α), piecewise s f g x ∂μ) = (∫ (x : α) in s, f x ∂μ) + ∫ (x : α) in sᶜ, g x ∂μ
rw [← Set.indicator_add_compl_eq_piecewise,
  integral_add' (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl),
  integral_indicator hs, integral_indicator hs.compl]