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
pos : ∀ (hnn : ¬s ≤[A] 0), False
⊢ s ≤[A] 0

Tactic:
by_contra hnn
-- 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
hnn : ¬s ≤[A] 0
⊢ ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j

Tactic:
rw [restrict_le_restrict_iff _ _ A_meas] at hnn

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- 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
hnn : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ A → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ A ∧ (↑0 : Set α → ℝ) j < (↑s : Set α → ℝ) j

Tactic:
push Not at hnn

Premises used: Not
-- 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
hnn : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ A ∧ (↑0 : Set α → ℝ) j < (↑s : Set α → ℝ) j
pos : ∀ (E : Set α) (hE₁ : MeasurableSet E) (hE₂ : E ⊆ A) (hE₃ : (↑0 : Set α → ℝ) E < (↑s : Set α → ℝ) E), False
⊢ False

Tactic:
obtain ⟨E, hE₁, hE₂, hE₃⟩ := hnn
-- 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
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
⊢ ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E

Tactic:
rw [tendsto_atTop_atTop] at h₄

Premises used: Filter.tendsto_atTop_atTop
-- 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₄ : ∀ (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
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
⊢ ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E

Tactic:
obtain ⟨k, hk⟩ := h₄ (max (1 / s E + 1) 1)

Premises used: MeasureTheory.VectorMeasure.measureOf', HDiv.hDiv, HAdd.hAdd, Max.max, OfNat.ofNat
-- 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₄ : ∀ (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

Tactic:
⟨k, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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₄ : ∀ (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
refine_2 : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
⊢ ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E

Tactic:
refine ⟨k, ?_, ?_⟩
-- 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₄ : ∀ (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) : ℝ)
⊢ LE.le (α := ℝ) 1 (↑(bdd k) : ℝ)

Tactic:
have hle := le_of_max_le_right (hk k le_rfl)
-- 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₄ : ∀ (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) : ℝ)
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (hle : 1 ≤ bdd k), 1 ≤ bdd k
⊢ 1 ≤ bdd k

Tactic:
norm_cast at hle
-- 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₄ : ∀ (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) : ℝ)
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
⊢ 1 / (↑s : Set α → ℝ) E < (↑(bdd k) : ℝ)

Tactic:
linarith only [le_of_max_le_left (hk k le_rfl)]

Premises used: le_rfl, le_of_max_le_left
-- 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₄ : ∀ (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) : ℝ)

Tactic:
have : 1 / s E < bdd k := by
        linarith only [le_of_max_le_left (hk k le_rfl)]
-- 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₄ : ∀ (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) : ℝ)
refine_2 : ∀ (this : ((↑s : Set α → ℝ) E)⁻¹ < (↑(bdd k) : ℝ)), (↑(bdd k) : ℝ)⁻¹ < (↑s : Set α → ℝ) E
⊢ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E

Tactic:
rw [one_div] at this ⊢

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 : ℕ) ↦ 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 : ((↑s : Set α → ℝ) E)⁻¹ < (↑(bdd k) : ℝ)
⊢ (↑(bdd k) : ℝ)⁻¹ < (↑s : Set α → ℝ) E

Tactic:
inv_lt_of_inv_lt₀ hE₃ this

Premises used: inv_lt_of_inv_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₄ : ∀ (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 : ((↑s : Set α → ℝ) E)⁻¹ < (↑(bdd k) : ℝ)
⊢ (↑(bdd k) : ℝ)⁻¹ < (↑s : Set α → ℝ) E

Tactic:
exact inv_lt_of_inv_lt₀ hE₃ this

Premises used: inv_lt_of_inv_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
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:
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
-- 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
this : ∃ (k : ℕ), 1 ≤ bdd k ∧ HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E
pos : ∀ (k : ℕ) (hk₁ : 1 ≤ bdd k) (hk₂ : HDiv.hDiv (α := ℝ) 1 (↑(bdd k) : ℝ) < (↑s : Set α → ℝ) E), False
⊢ False

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := this
-- 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
⊢ 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 _ _)