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
⊢ s ≤[A] 0
have pos : ∀ (hnn : ¬s ≤[A] 0), False
Tactic: by_contra hnn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
hnn : ¬s ≤[A] 0
⊢ False
have hnn₁ : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
Tactic: rw [restrict_le_restrict_iff _ _ A_meas] at hnn
Cleared hypotheses: hnn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
hnn : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
⊢ False
have hnn₁ : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ A ∧ (↑0 : Set α → ℝ) j < (↑s : Set α → ℝ) j
Tactic: push Not at hnn
Cleared hypotheses: hnn
-- 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
hnn : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ A ∧ (↑0 : Set α → ℝ) j < (↑s : Set α → ℝ) j
⊢ False
have pos : ∀ (E : Set α) (hE₁ : MeasurableSet E) (hE₂ : E ⊆ A) (hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E), False
Tactic: obtain ⟨E, hE₁, hE₂, hE₃⟩ := hnn
Cleared hypotheses: hnn
-- 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 : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
have rw : ∀ (h₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)) (A_meas : MeasurableSet A) (E : Set α)
  (hE₁ : MeasurableSet E) (hE₂ : E ⊆ A) (hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E),
  ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
Tactic: rw [tendsto_atTop_atTop] at h₄
Cleared hypotheses: h₄, A_meas, E, hE₁, hE₂, hE₃
-- 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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
⊢ ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
have obtain : ∀ (k : ℕ) (hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)),
  ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
Tactic: obtain ⟨k, hk⟩ := h₄ (max (1 / s E + 1) 1)
-- 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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
⊢ ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
have refine_1 : 1 ≤ bdd k
Tactic: refine ⟨k, ?_, ?_⟩
-- 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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
refine_1 : 1 ≤ bdd k
⊢ ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
have refine_2 : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
Tactic: refine ⟨k, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
⊢ 1 ≤ bdd k
have hle : LE.le (α := ℝ) 1 (↑(bdd k) : ℝ)
Tactic: have hle := le_of_max_le_right (hk k le_rfl)
-- 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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
hle : LE.le (α := ℝ) 1 (↑(bdd k) : ℝ)
⊢ 1 ≤ bdd k
have refine_1 : ∀ (hle : 1 ≤ bdd k), 1 ≤ bdd k
Tactic: norm_cast at hle
Cleared hypotheses: hle
-- 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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
⊢ 1 / (↑s : Set α → ℝ) E < (↑(bdd k) : ℝ)
have linarith : (↑(bdd k) : ℝ) ≤ 1 / (↑s : Set α → ℝ) E →
  -1 + (HMul.hMul (α := ℝ) 1 (↑(bdd k) : ℝ) - 1 * (1 / (↑s : Set α → ℝ) E)) +
      (1 * (1 / (↑s : Set α → ℝ) E) + HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑(bdd k) : ℝ)) =
    0
Tactic: linarith only [le_of_max_le_left (hk k le_rfl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
have this : 1 / (↑s : Set α → ℝ) E < (↑(bdd k) : ℝ)
Tactic: have : 1 / s E < bdd k := by
        linarith only [le_of_max_le_left (hk k le_rfl)]
-- 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₄ : ∀ (b : ℝ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → b ≤ (↑(bdd a) : ℝ)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / (↑s : Set α → ℝ) E + 1) 1 ≤ (↑(bdd a) : ℝ)
this : 1 / (↑s : Set α → ℝ) E < (↑(bdd k) : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
have refine_2 : ∀ (this : ((↑s : Set α → ℝ) E)⁻¹ < (↑(bdd k) : ℝ)), (↑(bdd k) : ℝ)⁻¹ < (↑s : Set α → ℝ) E
Tactic: rw [one_div] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ False
have this : ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
Tactic: have : ∃ k, 1 ≤ bdd k ∧ 1 / (bdd k : ℝ) < s E := by
    rw [tendsto_atTop_atTop] at h₄
    obtain ⟨k, hk⟩ := h₄ (max (1 / s E + 1) 1)
    refine ⟨k, ?_, ?_⟩
    · have hle := le_of_max_le_right (hk k le_rfl)
      norm_cast at hle
    · have : 1 / s E < bdd k := by
        linarith only [le_of_max_le_left (hk k le_rfl)]
      rw [one_div] at this ⊢
      exact inv_lt_of_inv_lt₀ hE₃ this
-- 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
this : ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
⊢ False
have pos : ∀ (k : ℕ) (hk₁ : 1 ≤ bdd k) (hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E), False
Tactic: obtain ⟨k, hk₁, hk₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ False
have hA' : A ⊆ i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l
Tactic: have hA' : A ⊆ i \ ⋃ l ≤ k, restrictNonposSeq s i l :=
    Set.diff_subset_diff_right (Set.iUnion₂_subset_iUnion _ _)
-- 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
⊢ False
have pos : 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ k), s.restrictNonposSeq i l) - 1) : ℝ) 1 <
  (↑s : Set α → ℝ) E
Tactic: refine
    findExistsOneDivLT_min (hn' k) (Nat.sub_lt hk₁ Nat.zero_lt_one)
      ⟨E, Set.Subset.trans hE₂ hA', hE₁, ?_⟩