no goals
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i n)
cases n with
| zero =>
  rw [restrictNonposSeq]; rw [← @Set.diff_empty _ i] at hi₂
  rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
  exact lt_trans Nat.one_div_pos_of_nat h
| succ n =>
  rw [restrictNonposSeq_succ]
  have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
    refine' mt (restrict_le_zero_subset _ _ (by simp [Nat.lt_succ_iff]; rfl)) hn
    convert measurable_of_not_restrict_le_zero _ hn using 3
    exact funext fun x => by rw [Nat.lt_succ_iff]
  rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
  exact lt_trans Nat.one_div_pos_of_nat h
case zero
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
case zero
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i Nat.zero)
rw [restrictNonposSeq]
case zero
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s (i \ ∅) ≤ restrict 0 (i \ ∅)
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
case zero
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
rw [← @Set.diff_empty _ i] at hi₂
case zero.intro.intro
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s (i \ ∅) ≤ restrict 0 (i \ ∅)
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
left✝¹ : MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅) ⊆ i \ ∅
left✝ : MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
h :
  1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ∅)) + 1) <
    ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
case zero
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s (i \ ∅) ≤ restrict 0 (i \ ∅)
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
no goals
case zero.intro.intro
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s (i \ ∅) ≤ restrict 0 (i \ ∅)
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.zero), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
left✝¹ : MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅) ⊆ i \ ∅
left✝ : MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
h :
  1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ∅)) + 1) <
    ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))
exact lt_trans Nat.one_div_pos_of_nat h
case succ
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
case succ
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i (Nat.succ n))
rw [restrictNonposSeq_succ]
case succ
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
h₁ :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
case succ
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
  refine' mt (restrict_le_zero_subset _ _ (by simp [Nat.lt_succ_iff]; rfl)) hn
  convert measurable_of_not_restrict_le_zero _ hn using 3
  exact funext fun x => by rw [Nat.lt_succ_iff]
case succ.intro.intro
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
h₁ :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
left✝¹ :
  MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
left✝ :
  MeasurableSet
    (MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
h :
  1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
case succ
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
h₁ :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
no goals
case succ.intro.intro
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
h₁ :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
left✝¹ :
  MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
left✝ :
  MeasurableSet
    (MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
h :
  1 /
      (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s
            (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) +
        1) <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
exact lt_trans Nat.one_div_pos_of_nat h
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ MeasurableSet (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ ¬restrict s (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
refine' mt (restrict_le_zero_subset _ _ (by simp [Nat.lt_succ_iff]; rfl)) hn
case h.e'_3.h.e'_4.h.e'_3
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ (fun k => ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) = fun k =>
    ⋃ (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ MeasurableSet (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
convert measurable_of_not_restrict_le_zero _ hn using 3
no goals
case h.e'_3.h.e'_4.h.e'_3
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ (fun k => ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) = fun k =>
    ⋃ (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
exact funext fun x => by rw [Nat.lt_succ_iff]
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
simp [Nat.lt_succ_iff]
no goals
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
⊢ (i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ⊆
    i \ ⋃ (k : ℕ) (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k
rfl
no goals
α : Type u_1
β : Type ?u.21389
inst✝³ : MeasurableSpace α
M : Type ?u.21395
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi₂ : ¬restrict s i ≤ restrict 0 i
n : ℕ
hn :
  ¬restrict s (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤
      restrict 0 (i \ ⋃ (k : ℕ) (_ : k < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
x : ℕ
⊢ (⋃ (_ : x ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i x) =
    ⋃ (_ : x < Nat.succ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i x
rw [Nat.lt_succ_iff]