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₂ : (↑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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
⊢ False

Tactic:
findExistsOneDivLT_min (hn' k) (Nat.sub_lt hk₁ Nat.zero_lt_one)
      ⟨E, Set.Subset.trans hE₂ hA', hE₁, ?_⟩

Premises used: Set.Subset.trans, Nat.sub_lt, _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT_min, And.intro, Exists.intro, Nat.zero_lt_one
-- 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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
pos :
  1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 <
    (↑s : Set α → ℝ) E
⊢ False

Tactic:
refine
    findExistsOneDivLT_min (hn' k) (Nat.sub_lt hk₁ Nat.zero_lt_one)
      ⟨E, Set.Subset.trans hE₂ hA', hE₁, ?_⟩

Premises used: Set.Subset.trans, Nat.sub_lt, _private.0.MeasureTheory.SignedMeasure.findExistsOneDivLT_min, And.intro, Exists.intro, Nat.zero_lt_one
-- 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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
⊢ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E

Tactic:
hk₂
-- 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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
h₅ :
  HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 =
    (↑(bdd k) : ℝ)
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 <
    (↑s : Set α → ℝ) E

Tactic:
convert! hk₂
-- 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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
h₅ : s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1 + 1 = bdd k
⊢ HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 =
    (↑(bdd k) : ℝ)

Tactic:
norm_cast
-- 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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
⊢ s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1 + 1 = bdd k

Tactic:
tsub_add_cancel_of_le hk₁

Premises used: tsub_add_cancel_of_le
-- 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
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk₁ : 1 ≤ bdd k
hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
⊢ s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1 + 1 = bdd k

Tactic:
exact tsub_add_cancel_of_le hk₁

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ 0 ∈ s.measureOfNegatives

Tactic:
⟨∅, ⟨MeasurableSet.empty, le_restrict_empty _ _⟩, s.empty⟩

Premises used: MeasureTheory.VectorMeasure.empty, MeasurableSet.empty, Set.Mem, setOf, MeasureTheory.VectorMeasure.le_restrict_empty, And.intro, Exists.intro, Set.image, MeasureTheory.SignedMeasure.measureOfNegatives, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
by_contra! : ∀ (h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x), False
⊢ ∃ (x : ℝ), ∀ x_1 ∈ s.measureOfNegatives, x ≤ x_1

Tactic:
by_contra! h
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
⊢ ∀ (n : ℕ), ∃ y ∈ s.measureOfNegatives, y < -(↑n : ℝ)

Tactic:
have h' : ∀ n : ℕ, ∃ y : ℝ, y ∈ s.measureOfNegatives ∧ y < -n := fun n => h (-n)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
h' : ∀ (n : ℕ), ∃ y ∈ s.measureOfNegatives, y < -(↑n : ℝ)
choose : ∀ (f : (n : ℕ) → ℝ) (hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)), False
⊢ False

Tactic:
choose f hf using h'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
n : ℕ
rcases :
  ∀ (hlt : f n < -(↑n : ℝ)) (B : Set α) (hB₂ : (↑s : Set α → ℝ) B = f n) (hB₁ : MeasurableSet B) (hBr : s ≤[B] 0),
    ∃ (B : Set α), MeasurableSet B ∧ s ≤[B] 0 ∧ (↑s : Set α → ℝ) B < -(↑n : ℝ)
⊢ ∃ (B : Set α), MeasurableSet B ∧ s ≤[B] 0 ∧ (↑s : Set α → ℝ) B < -(↑n : ℝ)

Tactic:
rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
n : ℕ
hlt : f n < -(↑n : ℝ)
B : Set α
hB₂ : (↑s : Set α → ℝ) B = f n
hB₁ : MeasurableSet B
hBr : s ≤[B] 0
⊢ ∃ (B : Set α), MeasurableSet B ∧ s ≤[B] 0 ∧ (↑s : Set α → ℝ) B < -(↑n : ℝ)

Tactic:
⟨B, hB₁, hBr, hB₂.symm ▸ hlt⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
n : ℕ
hlt : f n < -(↑n : ℝ)
B : Set α
hB₂ : (↑s : Set α → ℝ) B = f n
hB₁ : MeasurableSet B
hBr : s ≤[B] 0
⊢ ∃ (B : Set α), MeasurableSet B ∧ s ≤[B] 0 ∧ (↑s : Set α → ℝ) B < -(↑n : ℝ)

Tactic:
exact ⟨B, hB₁, hBr, hB₂.symm ▸ hlt⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
⊢ ∀ (n : ℕ), ∃ (B : Set α), MeasurableSet B ∧ s ≤[B] 0 ∧ (↑s : Set α → ℝ) B < -(↑n : ℝ)

Tactic:
have hf' : ∀ n : ℕ, ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ s B < -n := by
    intro n
    rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩
    exact ⟨B, hB₁, hBr, hB₂.symm ▸ hlt⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
hf' : ∀ (n : ℕ), ∃ (B : Set α), MeasurableSet B ∧ s ≤[B] 0 ∧ (↑s : Set α → ℝ) B < -(↑n : ℝ)
choose :
  ∀ (B : (n : ℕ) → Set α) (hmeas : ∀ (n : ℕ), MeasurableSet (B n)) (hr : ∀ (n : ℕ), s ≤[B n] 0)
    (h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)), False
⊢ False

Tactic:
choose B hmeas hr h_lt using hf'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
⊢ let A : Set α := ⋃ (n : ℕ), B n;
  A = ⋃ (n : ℕ), B n

Tactic:
set A := ⋃ n, B n with hA
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ (↑s : Set α → ℝ) A ≤ -(↑n : ℝ)

Tactic:
le_trans ?_ (le_of_lt (h_lt _))

Premises used: le_of_lt, le_trans
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
refine : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) (B n)
⊢ (↑s : Set α → ℝ) A ≤ -(↑n : ℝ)

Tactic:
refine le_trans ?_ (le_of_lt (h_lt _))

Premises used: le_of_lt, le_trans
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
rw : (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n) ≤ (↑s : Set α → ℝ) (B n)
rw₁ : MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
⊢ (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) (B n)

Tactic:
rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
      of_union Set.disjoint_sdiff_left _ (hmeas n)]

Premises used: MeasureTheory.VectorMeasure.of_union, Set.subset_iUnion, Set.disjoint_sdiff_left, Set.diff_union_of_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n) ≤ (↑s : Set α → ℝ) (B n)

Tactic:
add_le_of_nonpos_left ?_

Premises used: add_le_of_nonpos_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
refine : (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0
⊢ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n) ≤ (↑s : Set α → ℝ) (B n)

Tactic:
refine add_le_of_nonpos_left ?_

Premises used: add_le_of_nonpos_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ s ≤[A] 0

Tactic:
have : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hmeas hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : s ≤[A] 0
⊢ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0

Tactic:
nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)

Premises used: Set.diff_subset, MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero, MeasureTheory.VectorMeasure.restrict_le_zero_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : s ≤[A] 0
refine : MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)
⊢ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0

Tactic:
refine nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)

Premises used: Set.diff_subset, MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero, MeasureTheory.VectorMeasure.restrict_le_zero_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : s ≤[A] 0
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)

Tactic:
MeasurableSet.iUnion hmeas

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
this : s ≤[A] 0
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)

Tactic:
exact MeasurableSet.iUnion hmeas

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)

Tactic:
(MeasurableSet.iUnion hmeas).diff (hmeas n)

Premises used: MeasurableSet.diff, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
n : ℕ
⊢ MeasurableSet ((⋃ (i : ℕ), B i) \ B n)

Tactic:
exact (MeasurableSet.iUnion hmeas).diff (hmeas n)

Premises used: MeasurableSet.diff, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ ∀ (n : ℕ), (↑s : Set α → ℝ) A ≤ -(↑n : ℝ)

Tactic:
have hfalse : ∀ n : ℕ, s A ≤ -n := by
    intro n
    refine le_trans ?_ (le_of_lt (h_lt _))
    rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
      of_union Set.disjoint_sdiff_left _ (hmeas n)]
    · refine add_le_of_nonpos_left ?_
      have : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hmeas hr
      refine nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)
      exact MeasurableSet.iUnion hmeas
    · exact (MeasurableSet.iUnion hmeas).diff (hmeas n)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : (n : ℕ) → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)
B : (n : ℕ) → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hfalse : ∀ (n : ℕ), (↑s : Set α → ℝ) A ≤ -(↑n : ℝ)
rcases : ∀ (n : ℕ) (hn : -(↑s : Set α → ℝ) A < (↑n : ℝ)), False
⊢ False

Tactic:
rcases exists_nat_gt (-s A) with ⟨n, hn⟩

Premises used: MeasureTheory.VectorMeasure.measureOf', exists_nat_gt, Neg.neg