awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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
⊢ 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 <
    (↑s : Set α → ℝ) E
have h₅ : HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 =
  (↑(bdd k) : ℝ)
Tactic: convert! hk₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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
⊢ HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 =
    (↑(bdd k) : ℝ)
have h₅ : s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1 + 1 = bdd k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ (x : ℝ), ∀ x_1 ∈ s.measureOfNegatives, x ≤ x_1
have by_contra! : ∀ (h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
⊢ False
have h' : ∀ (n : ℕ), ∃ y ∈ s.measureOfNegatives, y < -(↑n : ℝ)
Tactic: have h' : ∀ n : ℕ, ∃ y : ℝ, y ∈ s.measureOfNegatives ∧ y < -n := fun n => h (-n)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
h' : ∀ (n : ℕ), ∃ y ∈ s.measureOfNegatives, y < -(↑n : ℝ)
⊢ False
have choose : ∀ (f : (n : ℕ) → ℝ) (hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -(↑n : ℝ)), False
Tactic: choose f hf using h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : ℝ)
have 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 : ℝ)
Tactic: rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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 : ℝ)
⊢ False
have hf' : ∀ (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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : ℝ)
⊢ False
have choose : ∀ (B : (n : ℕ) → Set α) (hmeas : ∀ (n : ℕ), MeasurableSet (B n)) (hr : ∀ (n : ℕ), s ≤[B n] 0)
  (h_lt : ∀ (n : ℕ), (↑s : Set α → ℝ) (B n) < -(↑n : ℝ)), False
Tactic: choose B hmeas hr h_lt using hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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 : ℝ)
⊢ False
have hA : let A : Set α := ⋃ (n : ℕ), B n;
A = ⋃ (n : ℕ), B n
Tactic: set A := ⋃ n, B n with hA
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : ℝ)
have refine : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) (B n)
Tactic: refine le_trans ?_ (le_of_lt (h_lt _))
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 ≤ (↑s : Set α → ℝ) (B n)
have rw : (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n) ≤ (↑s : Set α → ℝ) (B n)
Tactic: rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
      of_union Set.disjoint_sdiff_left _ (hmeas n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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)
⊢ (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) (B n)
have rw₁ : MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
Tactic: rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
      of_union Set.disjoint_sdiff_left _ (hmeas n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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)
have refine : (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0
Tactic: refine add_le_of_nonpos_left ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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) ≤ 0
have this : s ≤[A] 0
Tactic: have : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hmeas hr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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
have refine : MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), B i)
Tactic: refine nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ False
have hfalse : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : ℝ)
⊢ False
have rcases : ∀ (n : ℕ) (hn : -(↑s : Set α → ℝ) A < (↑n : ℝ)), False
Tactic: rcases exists_nat_gt (-s A) with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have obtain : ∀ (f : ℕ → ℝ),
  Antitone f →
    ∀ (hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))) (hf₁ : ∀ (n : ℕ), f n ∈ s.measureOfNegatives),
      ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
Tactic: obtain ⟨f, _, hf₂, hf₁⟩ :=
    exists_seq_tendsto_sInf ⟨0, @zero_mem_measureOfNegatives _ _ s⟩ bddBelow_measureOfNegatives
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
hf₁ : ∀ (n : ℕ), f n ∈ s.measureOfNegatives
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have choose : ∀ (B : (n : ℕ) → Set α)
  (hB :
    ∀ (n : ℕ),
      Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n),
  ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
Tactic: choose B hB using hf₁
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
Tactic: have hB₁ : ∀ n, MeasurableSet (B n) := fun n => (hB n).1.1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have hB₂ : ∀ (n : ℕ), s ≤[B n] 0
Tactic: have hB₂ : ∀ n, s ≤[B n] 0 := fun n => (hB n).1.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have hA : let A : Set α := ⋃ (n : ℕ), B n;
A = ⋃ (n : ℕ), B n
Tactic: set A := ⋃ n, B n with hA
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have hA₁ : MeasurableSet A
Tactic: have hA₁ : MeasurableSet A := MeasurableSet.iUnion hB₁
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have hA₂ : s ≤[A] 0
Tactic: have hA₂ : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hB₁ hB₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
have a : (↑s : Set α → ℝ) A ≤ sInf s.measureOfNegatives
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
a : (↑s : Set α → ℝ) A ≤ sInf s.measureOfNegatives
⊢ (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
have a₁ : sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) A
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ (↑s : Set α → ℝ) A ≤ sInf s.measureOfNegatives
have a : ∀ (n : ℕ), (fun (x : ℕ) ↦ (↑s : Set α → ℝ) A) n ≤ f n
Tactic: refine le_of_tendsto_of_tendsto tendsto_const_nhds hf₂ (Eventually.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun (x : ℕ) ↦ (↑s : Set α → ℝ) A) n ≤ f n
have a : (fun (x : ℕ) ↦ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n)) n ≤ (↑s : Set α → ℝ) (B n)
Tactic: rw [← (hB n).2, hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
        of_union Set.disjoint_sdiff_left _ (hB₁ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
a : (fun (x : ℕ) ↦ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n)) n ≤ (↑s : Set α → ℝ) (B n)
⊢ (fun (x : ℕ) ↦ (↑s : Set α → ℝ) A) n ≤ f n
have rw : MeasurableSet ((⋃ (i : ℕ), B i) \ B n)
Tactic: rw [← (hB n).2, hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
        of_union Set.disjoint_sdiff_left _ (hB₁ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
n : ℕ
⊢ (fun (x : ℕ) ↦ (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) + (↑s : Set α → ℝ) (B n)) n ≤ (↑s : Set α → ℝ) (B n)
have a : (↑s : Set α → ℝ) ((⋃ (i : ℕ), B i) \ B n) ≤ 0
Tactic: refine add_le_of_nonpos_left ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
Tactic: have hA₃ : s A = sInf s.measureOfNegatives := by
    apply le_antisymm
    · refine le_of_tendsto_of_tendsto tendsto_const_nhds hf₂ (Eventually.of_forall fun n => ?_)
      rw [← (hB n).2, hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n),
        of_union Set.disjoint_sdiff_left _ (hB₁ n)]
      · refine add_le_of_nonpos_left ?_
        have : s ≤[A] 0 :=
          restrict_le_restrict_iUnion _ _ hB₁ fun m =>
            let ⟨_, h⟩ := (hB m).1
            h
        refine
          nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)
        exact MeasurableSet.iUnion hB₁
      · exact (MeasurableSet.iUnion hB₁).diff (hB₁ n)
    · exact csInf_le bddBelow_measureOfNegatives ⟨A, ⟨hA₁, hA₂⟩, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
⊢ ∃ (i : Set α), MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
have refine : 0 ≤[Aᶜ] s
Tactic: refine ⟨Aᶜ, hA₁.compl, ?_, (compl_compl A).symm ▸ hA₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
⊢ 0 ≤[Aᶜ] s
have rw : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ Aᶜ → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
Tactic: rw [restrict_le_restrict_iff _ _ hA₁.compl]