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