awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l))
⊢ (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
apply le_add_of_nonneg_right

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
⊢ LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l))

Tactic:
tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))

Premises used: _private.0.MeasureTheory.SignedMeasure.measure_of_restrictNonposSeq, le_of_lt, tsum_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
⊢ LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l))

Tactic:
exact tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))

Premises used: _private.0.MeasureTheory.SignedMeasure.measure_of_restrictNonposSeq, le_of_lt, tsum_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
⊢ (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i

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))
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
⊢ Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
have : Summable fun l => s (restrictNonposSeq s i l) :=
      HasSum.summable
        (s.m_iUnion (fun _ => restrictNonposSeq_measurableSet _) restrictNonposSeq_disjoint)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
this : Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1

Tactic:
.of_nonneg_of_le (fun n => ?_) (fun n => ?_)
        (this.comp_injective Nat.succ_injective)

Premises used: Summable.of_nonneg_of_le, Nat.succ_injective, Summable.comp_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
this : Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
refine_1 : ∀ (n : ℕ), 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
refine_2 :
  ∀ (n : ℕ),
    1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1 ≤ ((fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)) ∘ Nat.succ) n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1

Tactic:
refine .of_nonneg_of_le (fun n => ?_) (fun n => ?_)
        (this.comp_injective Nat.succ_injective)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
this : Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
n : ℕ
⊢ 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1

Tactic:
le_of_lt Nat.one_div_pos_of_nat

Premises used: le_of_lt, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
this : Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
n : ℕ
⊢ 0 ≤ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1

Tactic:
exact le_of_lt Nat.one_div_pos_of_nat

Premises used: le_of_lt, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
this : Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
n : ℕ
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1 ≤ ((fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)) ∘ Nat.succ) n

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

Premises used: le_of_lt, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_lt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
this : Summable (α := ℝ) fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
n : ℕ
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1 ≤ ((fun (l : ℕ) ↦ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)) ∘ Nat.succ) n

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

Premises used: le_of_lt, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_lt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1

Tactic:
have h₃' : Summable fun n => (1 / (bdd n + 1) : ℝ) := by
    have : Summable fun l => s (restrictNonposSeq s i l) :=
      HasSum.summable
        (s.m_iUnion (fun _ => restrictNonposSeq_measurableSet _) restrictNonposSeq_disjoint)
    refine .of_nonneg_of_le (fun n => ?_) (fun n => ?_)
        (this.comp_injective Nat.succ_injective)
    · exact le_of_lt Nat.one_div_pos_of_nat
    · exact le_of_lt (restrictNonposSeq_lt n (hn' n))
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1)⁻¹

Tactic:
simp only [one_div] at h₃'

Premises used: one_div
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ (HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1)⁻¹
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop

Tactic:
Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)

Premises used: Nat.cast_add_one_pos, Summable.tendsto_atTop_of_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ (HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1)⁻¹
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop

Tactic:
exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)

Premises used: Nat.cast_add_one_pos, Summable.tendsto_atTop_of_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop

Tactic:
have h₃ : Tendsto (fun n => (bdd n : ℝ) + 1) atTop atTop := by
    simp only [one_div] at h₃'
    exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd x) : ℝ) 1 + -1) atTop atTop

Tactic:
atTop.tendsto_atTop_add_const_right (-1) h₃

Premises used: Filter.tendsto_atTop_add_const_right, Filter.atTop, OfNat.ofNat, Neg.neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
h₄ : ∀ (x : ℕ), (↑(bdd x) : ℝ) = HAdd.hAdd (α := ℝ) (↑(bdd x) : ℝ) 1 + -1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑(bdd n) : ℝ)) atTop atTop

Tactic:
convert! atTop.tendsto_atTop_add_const_right (-1) h₃

Premises used: Filter.tendsto_atTop_add_const_right, Filter.atTop, OfNat.ofNat, Neg.neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
x : ℕ
⊢ (↑(bdd x) : ℝ) = HAdd.hAdd (α := ℝ) (↑(bdd x) : ℝ) 1 + -1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑(bdd n) : ℝ)) atTop atTop

Tactic:
have h₄ : Tendsto (fun n => (bdd n : ℝ)) atTop atTop := by
    convert! atTop.tendsto_atTop_add_const_right (-1) h₃; simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
h₄ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑(bdd n) : ℝ)) atTop atTop
⊢ MeasurableSet A

Tactic:
have A_meas : MeasurableSet A :=
    hi₁.diff (MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
h₄ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑(bdd n) : ℝ)) atTop atTop
A_meas : MeasurableSet A
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
⟨A, A_meas, Set.diff_subset, ?_, h₂.trans_lt hi⟩

Premises used: Set.diff_subset, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
h₂ : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i
h₃' : Summable (α := ℝ) fun (n : ℕ) ↦ 1 / HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1
h₃ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑(bdd n) : ℝ) 1) atTop atTop
h₄ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑(bdd n) : ℝ)) atTop atTop
A_meas : MeasurableSet A
pos : s ≤[A] 0
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
refine ⟨A, A_meas, Set.diff_subset, ?_, h₂.trans_lt hi⟩