α : Type u_1
β : Type ?u.20255
inst✝³ : MeasurableSpace α
M : Type ?u.20261
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
α : Type u_1
β : Type ?u.20255
inst✝³ : MeasurableSpace α
M : Type ?u.20261
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i (Nat.succ n))
rw [restrictNonposSeq_succ]
no goals
α : Type u_1
β : Type ?u.20255
inst✝³ : MeasurableSpace α
M : Type ?u.20261
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
apply someExistsOneDivLT_lt hn