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

Tactic:
exact lt_trans Nat.one_div_pos_of_nat h

Result:
no goals

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
⊢ 0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i (n + 1))

Tactic:
rw [restrictNonposSeq_succ]

Result:
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
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (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
⊢ 0 <
    ↑s
      (MeasureTheory.SignedMeasure.someExistsOneDivLT s
        (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k))

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

Result:
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))

Proof state:
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 \ ∅))

Tactic:
exact lt_trans Nat.one_div_pos_of_nat h

Result:
no goals