∀ {α : Type u_1} {m : MeasurableSpace α} (s s_1 : MeasureTheory.SignedMeasure α) (e_s : s = s_1) (i i_1 : Set α)
  (e_i : i = i_1) (hi₁ : MeasurableSet i)
  (hi₂ : MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i),
  s.toMeasureOfLEZero i hi₁ hi₂ = s_1.toMeasureOfLEZero i_1 ⋯ ⋯