α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have hi₁ : MeasurableSet i := by_contradiction fun h => ne_of_lt hi <| s.not_measurable h
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : restrict s i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0

case neg
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
by_cases s ≤[i] 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0

case neg
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ¬∀ (n : ℕ),
      ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
          restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case neg
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
by_cases hn : ∀ n : ℕ, ¬s ≤[i \ ⋃ l < n, restrictNonposSeq s i l] 0
case neg
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ¬∀ (n : ℕ),
      ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
          restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0

case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0

case neg
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ¬∀ (n : ℕ),
      ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
          restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
swap
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
set A := i \ ⋃ l, restrictNonposSeq s i l with hA
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
set bdd : ℕ → ℕ := fun n => findExistsOneDivLT s (i \ ⋃ k ≤ n, restrictNonposSeq s i k)
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have h₁ : s i = s A + ∑' l, s (restrictNonposSeq s i l) := by
  rw [hA, ← s.of_disjoint_iUnion_nat, add_comm, of_add_of_diff]
  exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
  exacts [hi₁, Set.iUnion_subset fun _ => restrictNonposSeq_subset _, fun _ =>
    restrictNonposSeq_measurableSet _, restrictNonposSeq_disjoint]
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have h₂ : s A ≤ s i := by
  rw [h₁]
  apply le_add_of_nonneg_right
  exact tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have h₃ : Tendsto (fun n => (bdd n : ℝ) + 1) atTop atTop := by
  simp only [one_div] at h₃'
  exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have h₄ : Tendsto (fun n => (bdd n : ℝ)) atTop atTop := by
  convert atTop.tendsto_atTop_add_const_right (-1) h₃; simp
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have A_meas : MeasurableSet A :=
  hi₁.diff (MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _)
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
⊢ restrict s A ≤ restrict 0 A
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
refine' ⟨A, A_meas, Set.diff_subset _ _, _, h₂.trans_lt hi⟩
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn : ¬restrict s A ≤ restrict 0 A
⊢ False
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
⊢ restrict s A ≤ restrict 0 A
by_contra hnn
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → ↑s j ≤ ↑0 j
⊢ False
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn : ¬restrict s A ≤ restrict 0 A
⊢ False
rw [restrict_le_restrict_iff _ _ A_meas] at hnn
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn :
  Exists fun ⦃j⦄ =>
    MeasurableSet j ∧ (j ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ∧ ↑0 j < ↑s j
⊢ False
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → ↑s j ≤ ↑0 j
⊢ False
push_neg  at hnn
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
⊢ False
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
hnn :
  Exists fun ⦃j⦄ =>
    MeasurableSet j ∧ (j ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ∧ ↑0 j < ↑s j
⊢ False
obtain ⟨E, hE₁, hE₂, hE₃⟩ := hnn
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
⊢ False
case pos.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
this : ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < ↑s E
⊢ False
obtain ⟨k, hk₁, hk₂⟩ := this
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ False
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
⊢ False
have hA' : A ⊆ i \ ⋃ l ≤ k, restrictNonposSeq s i l := by
  apply Set.diff_subset_diff_right
  intro x; simp only [Set.mem_iUnion]
  rintro ⟨n, _, hn₂⟩
  exact ⟨n, hn₂⟩
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
              (i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) -
            1) +
        1) <
    ↑s E
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ False
refine'
  findExistsOneDivLT_min (hn' k) (Nat.sub_lt hk₁ Nat.zero_lt_one)
    ⟨E, Set.Subset.trans hE₂ hA', hE₁, _⟩
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ ↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) -
          1) +
      1 =
    ↑(bdd k)
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ 1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
              (i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) -
            1) +
        1) <
    ↑s E
convert hk₂
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ MeasureTheory.SignedMeasure.findExistsOneDivLT s
          (i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) -
        1 +
      1 =
    bdd k
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ ↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) -
          1) +
      1 =
    ↑(bdd k)
norm_cast
no goals
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
hA' : A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
⊢ MeasureTheory.SignedMeasure.findExistsOneDivLT s
          (i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) -
        1 +
      1 =
    bdd k
exact tsub_add_cancel_of_le hk₁
no goals
case pos
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : restrict s i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
exact ⟨i, hi₁, Set.Subset.refl _, h, hi⟩
no goals
case neg
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ¬∀ (n : ℕ),
      ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
          restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
exact exists_subset_restrict_nonpos' hi₁ hi hn
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
n : ℕ
⊢ ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
      restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
intro n
case h.e'_1.h.e'_4.h.e'_7.h.e'_4.h.e'_3.h.h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
n l : ℕ
x✝ : α
⊢ (x✝ ∈ ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ↔
    x✝ ∈ ⋃ (_ : l < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
case h.e'_1.h.e'_4.h.e'_7.h.e'_4.h.e'_3
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
n : ℕ
⊢ (fun l => ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) = fun l =>
    ⋃ (_ : l < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
ext l
case h.e'_1.h.e'_4.h.e'_7.h.e'_4.h.e'_3.h.h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
n l : ℕ
x✝ : α
⊢ x✝ ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l → (l ≤ n ↔ l < n + 1)
case h.e'_1.h.e'_4.h.e'_7.h.e'_4.h.e'_3.h.h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
n l : ℕ
x✝ : α
⊢ (x✝ ∈ ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ↔
    x✝ ∈ ⋃ (_ : l < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]
no goals
case h.e'_1.h.e'_4.h.e'_7.h.e'_4.h.e'_3.h.h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
n l : ℕ
x✝ : α
⊢ x✝ ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l → (l ≤ n ↔ l < n + 1)
exact fun _ => Nat.lt_succ_iff.symm
case hA
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ MeasurableSet (⋃ (i_1 : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case hB
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ MeasurableSet i

case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (⋃ (i_1 : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) ⊆ i

case hf₁
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case hf₂
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Pairwise (Disjoint on fun l => MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
rw [hA, ← s.of_disjoint_iUnion_nat, add_comm, of_add_of_diff]
case hB
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ MeasurableSet i

case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (⋃ (i_1 : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) ⊆ i

case hf₁
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case hf₂
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Pairwise (Disjoint on fun l => MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
case hA
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ MeasurableSet (⋃ (i_1 : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case hB
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ MeasurableSet i

case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (⋃ (i_1 : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) ⊆ i

case hf₁
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case hf₂
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Pairwise (Disjoint on fun l => MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
no goals
case hB
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ MeasurableSet i

case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (⋃ (i_1 : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) ⊆ i

case hf₁
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case hf₂
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Pairwise (Disjoint on fun l => MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
exacts [hi₁, Set.iUnion_subset fun _ => restrictNonposSeq_subset _, fun _ =>
  restrictNonposSeq_measurableSet _, restrictNonposSeq_disjoint]
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s A ≤ ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s A ≤ ↑s i
rw [h₁]
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ 0 ≤ ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s A ≤ ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
apply le_add_of_nonneg_right
no goals
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ 0 ≤ ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
exact tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Summable fun n => 1 / (↑(bdd n) + 1)
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
⊢ Summable fun n => 1 / (↑(bdd n) + 1)
have : Summable fun l => s (restrictNonposSeq s i l) :=
  HasSum.summable
    (s.m_iUnion (fun _ => restrictNonposSeq_measurableSet _) restrictNonposSeq_disjoint)
case refine'_1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
n : ℕ
⊢ 0 ≤ 1 / (↑(bdd n) + 1)

case refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
n : ℕ
⊢ 1 / (↑(bdd n) + 1) ≤ ((fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)) ∘ Nat.succ) n
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Summable fun n => 1 / (↑(bdd n) + 1)
refine'
  summable_of_nonneg_of_le (fun n => _) (fun n => _)
    (Summable.comp_injective this Nat.succ_injective)
no goals
case refine'_1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
n : ℕ
⊢ 0 ≤ 1 / (↑(bdd n) + 1)
exact le_of_lt Nat.one_div_pos_of_nat
no goals
case refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
n : ℕ
⊢ 1 / (↑(bdd n) + 1) ≤ ((fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)) ∘ Nat.succ) n
exact le_of_lt (restrictNonposSeq_lt n (hn' n))
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' :
  Summable fun n =>
    (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1)⁻¹
⊢ Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
⊢ Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
simp only [one_div] at h₃'
no goals
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' :
  Summable fun n =>
    (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1)⁻¹
⊢ Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)
case h.e'_3.h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
x✝ : ℕ
⊢ ↑(bdd x✝) = ↑(bdd x✝) + 1 + -1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
⊢ Tendsto (fun n => ↑(bdd n)) atTop atTop
convert atTop.tendsto_atTop_add_const_right (-1) h₃
no goals
case h.e'_3.h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
x✝ : ℕ
⊢ ↑(bdd x✝) = ↑(bdd x✝) + 1 + -1
simp
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
⊢ ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < ↑s E
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
⊢ ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < ↑s E
rw [tendsto_atTop_atTop] at h₄
case intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < ↑s E
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
⊢ ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < ↑s E
obtain ⟨k, hk⟩ := h₄ (max (1 / s E + 1) 1)
case intro.refine'_1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 ≤ bdd k

case intro.refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 / ↑(bdd k) < ↑s E
case intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ ∃ k, 1 ≤ bdd k ∧ 1 / ↑(bdd k) < ↑s E
refine' ⟨k, _, _⟩
case intro.refine'_1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
hle : 1 ≤ ↑(bdd k)
⊢ 1 ≤ bdd k
case intro.refine'_1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 ≤ bdd k
have hle := le_of_max_le_right (hk k le_rfl)
no goals
case intro.refine'_1
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
hle : 1 ≤ ↑(bdd k)
⊢ 1 ≤ bdd k
norm_cast at hle
case intro.refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
this : 1 / ↑s E < ↑(bdd k)
⊢ 1 / ↑(bdd k) < ↑s E
case intro.refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 / ↑(bdd k) < ↑s E
have : 1 / s E < bdd k := by
  linarith only [le_of_max_le_left (hk k le_rfl)]
case intro.refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
this : (↑s E)⁻¹ < ↑(bdd k)
⊢ (↑(bdd k))⁻¹ < ↑s E
case intro.refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
this : 1 / ↑s E < ↑(bdd k)
⊢ 1 / ↑(bdd k) < ↑s E
rw [one_div] at this ⊢
no goals
case intro.refine'_2
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
this : (↑s E)⁻¹ < ↑(bdd k)
⊢ (↑(bdd k))⁻¹ < ↑s E
rwa [inv_lt (lt_trans (inv_pos.2 hE₃) this) hE₃]
no goals
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / ↑s E + 1) 1 ≤ ↑(bdd a)
⊢ 1 / ↑s E < ↑(bdd k)
linarith only [le_of_max_le_left (hk k le_rfl)]
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
⊢ (⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ⊆
    ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
⊢ A ⊆ i \ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
apply Set.diff_subset_diff_right
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
x : α
⊢ (x ∈ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) →
    x ∈ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
⊢ (⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ⊆
    ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
intro x
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
x : α
⊢ (∃ i_1 i_2, x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) →
    ∃ i_1, x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
x : α
⊢ (x ∈ ⋃ (l : ℕ) (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) →
    x ∈ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
simp only [Set.mem_iUnion]
case h.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
x : α
n : ℕ
w✝ : n ≤ k
hn₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
⊢ ∃ i_1, x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1
case h
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
x : α
⊢ (∃ i_1 i_2, x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) →
    ∃ i_1, x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1
rintro ⟨n, _, hn₂⟩
no goals
case h.intro.intro
α : Type u_1
β : Type ?u.54598
inst✝³ : MeasurableSpace α
M : Type ?u.54604
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬restrict s i ≤ restrict 0 i
hn :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
A : Set α := i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' :
  ∀ (n : ℕ),
    ¬restrict s (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
        restrict 0 (i \ ⋃ (l : ℕ) (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ i \ ⋃ (l : ℕ), MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hE₃ : ↑0 E < ↑s E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : 1 / ↑(bdd k) < ↑s E
x : α
n : ℕ
w✝ : n ≤ k
hn₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
⊢ ∃ i_1, x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1
exact ⟨n, hn₂⟩