-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem exists_subset_restrict_nonpos (hi : s i < 0) :
    ∃ j : Set α, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ ↑s j < 0

Tactic:
have h₂ : s A ≤ s i := by
  rw [h₁]
  apply le_add_of_nonneg_right
  exact tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ ↑s j < 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ ↑s j < 0

Tactic:
by_cases h : s ≤[i] 0

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : s ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ ↑s j < 0

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
⊢ ∃ j, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ ↑s j < 0

Proof state:
case intro.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → (1 / ↑s E + 1) ⊔ 1 ≤ ↑(bdd a)
this : 1 / ↑s E < ↑(bdd k)
⊢ 1 / ↑(bdd k) < ↑s E

Tactic:
rw [one_div] at this ⊢

Result:
case intro.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
h₃' : Summable fun n => 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : ↑0 E < ↑s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → (1 / ↑s E + 1) ⊔ 1 ≤ ↑(bdd a)
this : (↑s E)⁻¹ < ↑(bdd k)
⊢ (↑(bdd k))⁻¹ < ↑s E

Proof state:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ↑s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l
bdd : ℕ → ℕ :=
  fun n =>
    MeasureTheory.SignedMeasure.findExistsOneDivLT s
      (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l] 0
h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
h₂ : ↑s A ≤ ↑s i
this : Summable fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)
n : ℕ
⊢ 1 / (↑(bdd n) + 1) ≤ ((fun l => ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)) ∘ Nat.succ) n

Tactic:
exact le_of_lt (restrictNonposSeq_lt n (hn' n))

Result:
no goals