awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
neg : a < k → Disjoint (s.restrictNonposSeq i a) ((fun (l : ℕ) ↦ (⋃ (_ : l < k), s.restrictNonposSeq i l : Set α)) b)
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (l : ℕ) ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) a b

Tactic:
refine Set.disjoint_iUnion_left.mpr fun _ => ?_

Premises used: Iff.mpr, Set.disjoint_iUnion_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
h_1 : a < k
⊢ Disjoint (s.restrictNonposSeq i a) ((fun (l : ℕ) ↦ (⋃ (_ : l < k), s.restrictNonposSeq i l : Set α)) b)

Tactic:
Set.disjoint_iUnion_right.mpr fun _ => ?_

Premises used: Iff.mpr, Set.disjoint_iUnion_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
h_1 : a < k
neg : b < k → Disjoint (s.restrictNonposSeq i a) (s.restrictNonposSeq i b)
⊢ Disjoint (s.restrictNonposSeq i a) ((fun (l : ℕ) ↦ (⋃ (_ : l < k), s.restrictNonposSeq i l : Set α)) b)

Tactic:
refine Set.disjoint_iUnion_right.mpr fun _ => ?_

Premises used: Iff.mpr, Set.disjoint_iUnion_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
h_1 : a < k
h_2 : b < k
⊢ Disjoint (s.restrictNonposSeq i a) (s.restrictNonposSeq i b)

Tactic:
restrictNonposSeq_disjoint hab

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
h_1 : a < k
h_2 : b < k
⊢ Disjoint (s.restrictNonposSeq i a) (s.restrictNonposSeq i b)

Tactic:
exact restrictNonposSeq_disjoint hab

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
neg : ∀ (i_1 : ℕ), ⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1 ⊆ i
⊢ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l ⊆ i

Tactic:
apply Set.iUnion_subset

Premises used: Set.iUnion_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a : ℕ
x : α
neg : a < k → x ∈ s.restrictNonposSeq i a → x ∈ i
⊢ Membership.mem (γ := Set α) (⋃ (_ : a < k), s.restrictNonposSeq i a) x → x ∈ i

Tactic:
simp only [and_imp, exists_prop, Set.mem_iUnion]

Premises used: and_imp, Set.mem_iUnion, exists_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a : ℕ
x : α
h_1 : a < k
hx : x ∈ s.restrictNonposSeq i a
⊢ x ∈ i

Tactic:
restrictNonposSeq_subset _ hx

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
h : ¬s ≤[i] 0
hn : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find (p := fun (n : ℕ) ↦ s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0) hn
hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
a : ℕ
x : α
h_1 : a < k
hx : x ∈ s.restrictNonposSeq i a
⊢ x ∈ i

Tactic:
exact restrictNonposSeq_subset _ hx

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
⊢ MeasurableSet i

Tactic:
have hi₁ : MeasurableSet i := by_contradiction fun h => ne_of_lt hi <| s.not_measurable h
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
pos : ∀ (h : s ≤[i] 0), ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
neg : ∀ (h : ¬s ≤[i] 0), ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
by_cases h : s ≤[i] 0
-- 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
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
⟨i, hi₁, Set.Subset.refl _, h, hi⟩

Premises used: Set.Subset.refl, 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
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
exact ⟨i, hi₁, Set.Subset.refl _, h, hi⟩
-- 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
pos :
  ∀ (hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0),
    ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
neg :
  ∀ (hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0),
    ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
by_cases hn : ∀ n : ℕ, ¬s ≤[i \ ⋃ l < n, restrictNonposSeq s i l] 0
-- 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
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
exists_subset_restrict_nonpos' hi₁ hi hn

Premises used: _private.0.MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos'
-- 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
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
exact exists_subset_restrict_nonpos' hi₁ hi hn

Premises used: _private.0.MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos'
-- 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
⊢ let A := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l;
  A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l

Tactic:
set A := i \ ⋃ l, restrictNonposSeq s i l with hA
-- 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)
n : ℕ
⊢ ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n + 1), s.restrictNonposSeq i l] 0

Tactic:
hn (n + 1)

Premises used: HAdd.hAdd, 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)
n : ℕ
h₁ h₂ :
  Eq.{u_1 + 1} (α := ℕ → Set α) (fun (l : ℕ) ↦ ⋃ (_ : l ≤ n), s.restrictNonposSeq i l) fun (l : ℕ) ↦
    ⋃ (_ : l < n + 1), s.restrictNonposSeq i l
⊢ ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0

Tactic:
convert! hn (n + 1) using 5

Premises used: HAdd.hAdd, 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)
n : ℕ
h₁ :
  ∀ (l : ℕ) (x : α),
    Membership.mem (γ := Set α) (⋃ (_ : l ≤ n), s.restrictNonposSeq i l) x ↔
      Membership.mem (γ := Set α) (⋃ (_ : l < n + 1), s.restrictNonposSeq i l) x
⊢ Eq.{u_1 + 1} (α := ℕ → Set α) (fun (l : ℕ) ↦ ⋃ (_ : l ≤ n), s.restrictNonposSeq i l) fun (l : ℕ) ↦
    ⋃ (_ : l < n + 1), s.restrictNonposSeq i l

Tactic:
ext l
-- 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)
n l : ℕ
x : α
h₁ : x ∈ s.restrictNonposSeq i l → (l ≤ n ↔ l < n + 1)
⊢ Membership.mem (γ := Set α) (⋃ (_ : l ≤ n), s.restrictNonposSeq i l) x ↔
    Membership.mem (γ := Set α) (⋃ (_ : l < n + 1), s.restrictNonposSeq i l) x

Tactic:
simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]

Premises used: Set.mem_iUnion, exists_prop, and_congr_left_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)
n l : ℕ
x : α
⊢ x ∈ s.restrictNonposSeq i l → (l ≤ n ↔ l < n + 1)

Tactic:
fun _ => Nat.lt_succ_iff.symm

Premises used: Nat.lt_succ_iff, Iff.symm
-- 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)
n l : ℕ
x : α
⊢ x ∈ s.restrictNonposSeq i l → (l ≤ n ↔ l < n + 1)

Tactic:
exact fun _ => Nat.lt_succ_iff.symm

Premises used: Nat.lt_succ_iff, Iff.symm
-- 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)
⊢ ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0

Tactic:
have hn' : ∀ n : ℕ, ¬s ≤[i \ ⋃ l ≤ n, restrictNonposSeq s i l] 0 := by
    intro n
    convert! hn (n + 1) using 5 <;>
      · ext l
        simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]
        exact fun _ => Nat.lt_succ_iff.symm
-- 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
hA₁ : MeasurableSet.{u_1} (α := α) (⋃ (i_1 : ℕ), s.restrictNonposSeq i i_1)
hB : MeasurableSet i
h₁ : ⋃ (i_1 : ℕ), s.restrictNonposSeq i i_1 ⊆ i
hm : ∀ (i_1 : ℕ), MeasurableSet (s.restrictNonposSeq i i_1)
hd : Pairwise (Function.onFun Disjoint (s.restrictNonposSeq i))
⊢ (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
rw [hA, ← s.of_disjoint_iUnion, add_comm, of_add_of_diff]

Premises used: add_comm, MeasureTheory.VectorMeasure.of_disjoint_iUnion, MeasureTheory.VectorMeasure.of_add_of_diff
-- 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
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i_1 : ℕ), s.restrictNonposSeq i i_1)

Tactic:
MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_measurableSet, MeasurableSet.iUnion
-- 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
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i_1 : ℕ), s.restrictNonposSeq i i_1)

Tactic:
exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_measurableSet, MeasurableSet.iUnion
-- 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
⊢ MeasurableSet i

Tactic:
hi₁
-- 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
⊢ ⋃ (i_1 : ℕ), s.restrictNonposSeq i i_1 ⊆ i

Tactic:
Set.iUnion_subset fun _ => restrictNonposSeq_subset _

Premises used: Set.iUnion_subset, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_subset
-- 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
⊢ ∀ (i_1 : ℕ), MeasurableSet (s.restrictNonposSeq i i_1)

Tactic:
fun _ =>
      restrictNonposSeq_measurableSet _

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

Tactic:
restrictNonposSeq_disjoint

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

Tactic:
exacts [hi₁, Set.iUnion_subset fun _ => restrictNonposSeq_subset _, fun _ =>
      restrictNonposSeq_measurableSet _, restrictNonposSeq_disjoint]

Premises used: Set.iUnion_subset, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_measurableSet, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_subset
-- 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
⊢ (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
have h₁ : s i = s A + ∑' l, s (restrictNonposSeq s i l) := by
    rw [hA, ← s.of_disjoint_iUnion, add_comm, of_add_of_diff]
    · exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
    exacts [hi₁, Set.iUnion_subset fun _ => restrictNonposSeq_subset _, fun _ =>
      restrictNonposSeq_measurableSet _, restrictNonposSeq_disjoint]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : (↑s : Set α → ℝ) i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
hA : A = i \ ⋃ (l : ℕ), s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun (n : ℕ) ↦ s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : (↑s : Set α → ℝ) i = (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
rw : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) A + ∑' (l : ℕ), (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
⊢ (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) i

Tactic:
rw [h₁]