case pos
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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 : 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.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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 : ¬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.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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
by_cases s ≤[i] 0
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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 : ¬restrict s i ≤ restrict 0 i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
push_neg  at hn
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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 k := Nat.find hn
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), 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.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have hk₂ : s ≤[i \ ⋃ l < k, restrictNonposSeq s i l] 0 := Nat.find_spec hn
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), 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.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
have hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), restrictNonposSeq s i l) :=
  MeasurableSet.iUnion fun _ => MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) < 0
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ restrict s j ≤ restrict 0 j ∧ ↑s j < 0
refine' ⟨i \ ⋃ l < k, restrictNonposSeq s i l, hi₁.diff hmeas, Set.diff_subset _ _, hk₂, _⟩
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (↑s i - ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)) < 0

case neg.hf₁
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)

case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Pairwise (Disjoint on fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)

case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ⊆ i
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) < 0
rw [of_diff hmeas hi₁, s.of_disjoint_iUnion_nat]
no goals
case pos
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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 : 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₂⟩
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (↑s i - ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)) < 0
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (↑s i - ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)) < 0
have h₁ : ∀ l < k, 0 ≤ s (restrictNonposSeq s i l) := by
  intro l hl
  refine' le_of_lt (measure_of_restrictNonposSeq h _ _)
  refine' mt (restrict_le_zero_subset _ (hi₁.diff _) (Set.Subset.refl _)) (Nat.find_min hn hl)
  exact
    MeasurableSet.iUnion fun _ =>
      MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ 0 ≤ ∑' (l : ℕ), ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (↑s i - ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)) < 0
suffices 0 ≤ ∑' l : ℕ, s (⋃ _ : l < k, restrictNonposSeq s i l) by
  rw [sub_neg]
  exact lt_of_lt_of_le hi₂ this
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), 0 ≤ ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ 0 ≤ ∑' (l : ℕ), ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
refine' tsum_nonneg _
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), 0 ≤ ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)
intro l
case pos
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)

case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
by_cases l < k
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
intro l hl
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
refine' le_of_lt (measure_of_restrictNonposSeq h _ _)
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ MeasurableSet (⋃ (k : ℕ) (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
refine' mt (restrict_le_zero_subset _ (hi₁.diff _) (Set.Subset.refl _)) (Nat.find_min hn hl)
no goals
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
hl : l < k
⊢ MeasurableSet (⋃ (k : ℕ) (_ : k < l), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
exact
  MeasurableSet.iUnion fun _ =>
    MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
this : 0 ≤ ∑' (l : ℕ), ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s i < ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
this : 0 ≤ ∑' (l : ℕ), ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (↑s i - ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)) < 0
rw [sub_neg]
no goals
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
this : 0 ≤ ∑' (l : ℕ), ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ↑s i < ∑' (i_1 : ℕ), ↑s (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)
exact lt_of_lt_of_le hi₂ this
case h.e'_4.h.e'_7
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) =
    MeasureTheory.SignedMeasure.restrictNonposSeq s i l
case pos
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
convert h₁ _ h
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
x : α
⊢ (x ∈ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ↔
    x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l
case h.e'_4.h.e'_7
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
⊢ (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) =
    MeasureTheory.SignedMeasure.restrictNonposSeq s i l
ext x
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l → l < k
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
x : α
⊢ (x ∈ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ↔
    x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l
rw [Set.mem_iUnion, exists_prop, and_iff_right_iff_imp]
no goals
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l → l < k
exact fun _ => h
case h.e'_4.h.e'_7
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
⊢ (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) = ∅
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
⊢ 0 ≤ ↑s (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
convert le_of_eq s.empty.symm
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
x✝ : α
⊢ (x✝ ∈ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ↔ x✝ ∈ ∅
case h.e'_4.h.e'_7
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
⊢ (⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) = ∅
ext
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
x✝ : α
⊢ l < Nat.find hn → ¬x✝ ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
x✝ : α
⊢ (x✝ ∈ ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ↔ x✝ ∈ ∅
simp only [exists_prop, Set.mem_empty_iff_false, Set.mem_iUnion, not_and, iff_false_iff]
no goals
case h.e'_4.h.e'_7.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₁ : ∀ (l : ℕ), l < k → 0 ≤ ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
l : ℕ
h : ¬l < k
x✝ : α
⊢ l < Nat.find hn → ¬x✝ ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i l
exact fun h' => False.elim (h h')
case neg.hf₁
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
i✝ : ℕ
⊢ MeasurableSet (⋃ (_ : i✝ < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i✝)
case neg.hf₁
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1)
intro
no goals
case neg.hf₁
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
i✝ : ℕ
⊢ MeasurableSet (⋃ (_ : i✝ < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i✝)
exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
⊢ (Disjoint on fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) a b
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ Pairwise (Disjoint on fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
intro a b hab
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
x✝ : a < k
⊢ Disjoint (MeasureTheory.SignedMeasure.restrictNonposSeq s i a)
    ((fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) b)
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
⊢ (Disjoint on fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) a b
refine' Set.disjoint_iUnion_left.mpr fun _ => _
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
x✝¹ : a < k
x✝ : b < k
⊢ Disjoint (MeasureTheory.SignedMeasure.restrictNonposSeq s i a) (MeasureTheory.SignedMeasure.restrictNonposSeq s i b)
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
x✝ : a < k
⊢ Disjoint (MeasureTheory.SignedMeasure.restrictNonposSeq s i a)
    ((fun l => ⋃ (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) b)
refine' Set.disjoint_iUnion_right.mpr fun _ => _
no goals
case neg.hf₂
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a b : ℕ
hab : a ≠ b
x✝¹ : a < k
x✝ : b < k
⊢ Disjoint (MeasureTheory.SignedMeasure.restrictNonposSeq s i a) (MeasureTheory.SignedMeasure.restrictNonposSeq s i b)
exact restrictNonposSeq_disjoint hab
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) ⊆ i
case neg
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ⊆ i
apply Set.iUnion_subset
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
⊢ (x ∈ ⋃ (_ : a < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i a) → x ∈ i
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∀ (i_1 : ℕ), (⋃ (_ : i_1 < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i i_1) ⊆ i
intro a x
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
⊢ a < Nat.find hn → x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i a → x ∈ i
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
⊢ (x ∈ ⋃ (_ : a < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i a) → x ∈ i
simp only [and_imp, exists_prop, Set.mem_iUnion]
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
a✝ : a < Nat.find hn
hx : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i a
⊢ x ∈ i
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
⊢ a < Nat.find hn → x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i a → x ∈ i
intro _ hx
no goals
case neg.h
α : Type u_1
β : Type ?u.39511
inst✝³ : MeasurableSpace α
M : Type ?u.39517
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₁ : MeasurableSet i
hi₂ : ↑s i < 0
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)
k : ℕ := Nat.find hn
hk₂ :
  restrict s (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤
    restrict 0 (i \ ⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
a : ℕ
x : α
a✝ : a < Nat.find hn
hx : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i a
⊢ x ∈ i
exact restrictNonposSeq_subset _ hx