no goals
α : Type u_1
β : Type ?u.18814
inst✝³ : MeasurableSpace α
M : Type ?u.18820
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i (Nat.succ n) =
    MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
rw [restrictNonposSeq]