case succ
α : Type u_1
β : Type ?u.36367
inst✝³ : MeasurableSpace α
M : Type ?u.36373
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n✝ : ℕ
⊢ MeasurableSet
    (MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ (k : ℕ) (H : k ≤ n✝),
          let_fun this := (_ : k < Nat.succ n✝);
          MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
case succ
α : Type u_1
β : Type ?u.36367
inst✝³ : MeasurableSpace α
M : Type ?u.36373
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n✝ : ℕ
⊢ MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i (Nat.succ n✝))
rw [restrictNonposSeq]
no goals
case succ
α : Type u_1
β : Type ?u.36367
inst✝³ : MeasurableSpace α
M : Type ?u.36373
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n✝ : ℕ
⊢ MeasurableSet
    (MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ (k : ℕ) (H : k ≤ n✝),
          let_fun this := (_ : k < Nat.succ n✝);
          MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
exact someExistsOneDivLT_measurableSet