∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {s t : Set X} {μ : MeasureTheory.Measure X} {f : X → E},
  MeasurableSet t → (∀ x ∈ t, f x = 0) → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ