-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem measure_of_restrictNonposSeq (hi₂ : ¬s ≤[i] 0) (n : ℕ)
    (hn : ¬s ≤[i \ ⋃ k < n, restrictNonposSeq s i k] 0) : 0 < s (restrictNonposSeq s i n)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0

Tactic:
refine mt (restrict_le_zero_subset _ ?_ (by simp [Nat.lt_succ_iff])) hn

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ MeasurableSet (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
h₁ : ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))

Tactic:
rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩

Result:
case succ.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
h₁ : ¬s ≤[i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
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))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i n)

Tactic:
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])) 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

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k ⊆
    i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k

Tactic:
simp [Nat.lt_succ_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ MeasurableSet (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)

Tactic:
convert measurable_of_not_restrict_le_zero _ hn using 3

Result:
case h.e'_3.h.e'_4.h.e'_3
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ (fun k => ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) = fun k =>
    ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i 0)

Tactic:
rw [restrictNonposSeq]

Result:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
x : ℕ
⊢ ⋃ (_ : x ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i x =
    ⋃ (_ : x < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i x

Tactic:
rw [Nat.lt_succ_iff]

Result:
no goals

Proof state:
case h.e'_3.h.e'_4.h.e'_3
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ (fun k => ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) = fun k =>
    ⋃ (_ : k < n + 1), MeasureTheory.SignedMeasure.restrictNonposSeq s i k

Tactic:
exact funext fun x => by rw [Nat.lt_succ_iff]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))

Tactic:
rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩

Result:
case zero.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
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 \ ∅))

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))

Tactic:
rw [← @Set.diff_empty _ i] at hi₂

Result:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ k, ⋃ (_ : k < 0), MeasureTheory.SignedMeasure.restrictNonposSeq s i k] 0
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ∅))