α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n < m
⊢ ∀ (x : α),
    ¬x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n < m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
rw [Set.eq_empty_iff_forall_not_mem]
case intro
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n < m
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i m
⊢ False
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n < m
⊢ ∀ (x : α),
    ¬x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m
rintro x ⟨hx₁, hx₂⟩
case intro.zero
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
h : n < Nat.zero
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i Nat.zero
⊢ False

case intro.succ
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
n✝ : ℕ
h : n < Nat.succ n✝
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i (Nat.succ n✝)
⊢ False
case intro
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n m : ℕ
h : n < m
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i m
⊢ False
cases m
case intro.zero
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
h : n < 0
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i Nat.zero
⊢ False
case intro.zero
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
h : n < Nat.zero
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i Nat.zero
⊢ False
rw [Nat.zero_eq] at h
no goals
case intro.zero
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
h : n < 0
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i Nat.zero
⊢ False
linarith
case intro.succ
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
n✝ : ℕ
h : n < Nat.succ n✝
hx₂ :
  x ∈
    MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ (k : ℕ) (H : k ≤ n✝),
          let_fun this := (_ : k < Nat.succ n✝);
          MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ False
case intro.succ
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
n✝ : ℕ
h : n < Nat.succ n✝
hx₂ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i (Nat.succ n✝)
⊢ False
rw [restrictNonposSeq] at hx₂
no goals
case intro.succ
α : Type u_1
β : Type ?u.36768
inst✝³ : MeasurableSpace α
M : Type ?u.36774
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
n : ℕ
x : α
hx₁ : x ∈ MeasureTheory.SignedMeasure.restrictNonposSeq s i n
n✝ : ℕ
h : n < Nat.succ n✝
hx₂ :
  x ∈
    MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ (k : ℕ) (H : k ≤ n✝),
          let_fun this := (_ : k < Nat.succ n✝);
          MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ False
exact
  (someExistsOneDivLT_subset hx₂).2
    (Set.mem_iUnion.2 ⟨n, Set.mem_iUnion.2 ⟨Nat.lt_succ_iff.mp h, hx₁⟩⟩)