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)
l : ℕ
hl : l < k
⊢ 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
le_of_lt (measure_of_restrictNonposSeq h _ ?_)

Premises used: _private.0.MeasureTheory.SignedMeasure.measure_of_restrictNonposSeq, le_of_lt
-- 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)
l : ℕ
hl : l < k
refine : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k] 0
⊢ 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
refine le_of_lt (measure_of_restrictNonposSeq h _ ?_)

Premises used: _private.0.MeasureTheory.SignedMeasure.measure_of_restrictNonposSeq, le_of_lt
-- 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)
l : ℕ
hl : l < k
⊢ ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k] 0

Tactic:
mt (restrict_le_zero_subset _ (hi₁.diff ?_) (Set.Subset.refl _)) (Nat.find_min hn hl)

Premises used: MeasurableSet.diff, Set.Subset.refl, mt, MeasureTheory.VectorMeasure.restrict_le_zero_subset, Nat.find_min
-- 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)
l : ℕ
hl : l < k
refine : MeasurableSet.{u_1} (α := α) (⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k)
⊢ ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k] 0

Tactic:
refine mt (restrict_le_zero_subset _ (hi₁.diff ?_) (Set.Subset.refl _)) (Nat.find_min hn hl)

Premises used: MeasurableSet.diff, Set.Subset.refl, mt, MeasureTheory.VectorMeasure.restrict_le_zero_subset, Nat.find_min
-- 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)
l : ℕ
hl : l < k
⊢ MeasurableSet.{u_1} (α := α) (⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k)

Tactic:
MeasurableSet.iUnion fun _ =>
          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₁ : 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)
l : ℕ
hl : l < k
⊢ MeasurableSet.{u_1} (α := α) (⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k)

Tactic:
exact
        MeasurableSet.iUnion fun _ =>
          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₁ : 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)
⊢ ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
have h₁ : ∀ l < k, 0 ≤ s (restrictNonposSeq s i l) := by
      intro l hl
      refine le_of_lt (measure_of_restrictNonposSeq h _ ?_)
      refine mt (restrict_le_zero_subset _ (hi₁.diff ?_) (Set.Subset.refl _)) (Nat.find_min hn hl)
      exact
        MeasurableSet.iUnion fun _ =>
          MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
this : LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l))
rw : (↑s : Set α → ℝ) i < ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)
⊢ (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0

Tactic:
rw [sub_neg]

Premises used: sub_neg
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
this : LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l))
⊢ (↑s : Set α → ℝ) i < ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)

Tactic:
lt_of_lt_of_le hi₂ this

Premises used: lt_of_lt_of_le
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
this : LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l))
⊢ (↑s : Set α → ℝ) i < ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)

Tactic:
exact lt_of_lt_of_le hi₂ this

Premises used: lt_of_lt_of_le
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
neg : LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l))
⊢ (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0

Tactic:
suffices 0 ≤ ∑' l : ℕ, s (⋃ _ : l < k, restrictNonposSeq s i l) by
      rw [sub_neg]
      exact lt_of_lt_of_le hi₂ this
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
⊢ LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l))

Tactic:
tsum_nonneg ?_

Premises used: tsum_nonneg
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
neg : ∀ (i_1 : ℕ), 0 ≤ (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)
⊢ LE.le (α := ℝ) 0 (∑' (l : ℕ), (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l))

Tactic:
refine tsum_nonneg ?_

Premises used: tsum_nonneg
-- 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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
pos : ∀ (h : l < k), 0 ≤ (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l)
neg : ∀ (h : ¬l < k), 0 ≤ (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ 0 ≤ (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l)

Tactic:
by_cases h : l < k
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : l < k
⊢ 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)

Tactic:
h₁ _ h
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : l < k
h₂ : ⋃ (_ : l < k), s.restrictNonposSeq i l = s.restrictNonposSeq i l
⊢ 0 ≤ (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l)

Tactic:
convert! h₁ _ h
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : l < k
h₂ : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (_ : l < k), s.restrictNonposSeq i l) x ↔ x ∈ s.restrictNonposSeq i l
⊢ ⋃ (_ : l < k), s.restrictNonposSeq i l = s.restrictNonposSeq i l

Tactic:
ext x
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
h₂ : x ∈ s.restrictNonposSeq i l → l < k
⊢ Membership.mem (γ := Set α) (⋃ (_ : l < k), s.restrictNonposSeq i l) x ↔ x ∈ s.restrictNonposSeq i l

Tactic:
rw [Set.mem_iUnion, exists_prop, and_iff_right_iff_imp]

Premises used: Set.mem_iUnion, exists_prop, and_iff_right_iff_imp
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ s.restrictNonposSeq i l → l < k

Tactic:
fun _ => h
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
⊢ x ∈ s.restrictNonposSeq i l → l < k

Tactic:
exact fun _ => h
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
⊢ 0 ≤ (↑s : Set α → ℝ) ∅

Tactic:
le_of_eq s.empty.symm

Premises used: MeasureTheory.VectorMeasure.empty, le_of_eq, Eq.symm
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
h₂ : Eq.{u_1 + 1} (α := Set α) (⋃ (_ : l < k), s.restrictNonposSeq i l) ∅
⊢ 0 ≤ (↑s : Set α → ℝ) (⋃ (_ : l < k), s.restrictNonposSeq i l)

Tactic:
convert! le_of_eq s.empty.symm

Premises used: MeasureTheory.VectorMeasure.empty, le_of_eq, Eq.symm
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
h₂ : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (_ : l < k), s.restrictNonposSeq i l) x ↔ Membership.mem (γ := Set α) ∅ x
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (_ : l < k), s.restrictNonposSeq i l) ∅

Tactic:
ext
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
x : α
h₂ : l < k → x ∉ s.restrictNonposSeq i l
⊢ Membership.mem (γ := Set α) (⋃ (_ : l < k), s.restrictNonposSeq i l) x ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simp only [exists_prop, Set.mem_empty_iff_false, Set.mem_iUnion, not_and, iff_false]

Premises used: iff_false, Set.mem_iUnion, exists_prop, Set.mem_empty_iff_false, not_and
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
x : α
⊢ l < k → x ∉ s.restrictNonposSeq i l

Tactic:
fun h' => False.elim (h h')

Premises used: False.elim
-- 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_1 : ¬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)
h₁ : ∀ l < k, 0 ≤ (↑s : Set α → ℝ) (s.restrictNonposSeq i l)
l : ℕ
h : ¬l < k
x : α
⊢ l < k → x ∉ s.restrictNonposSeq i l

Tactic:
exact fun h' => False.elim (h h')

Premises used: False.elim
-- 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)
i_1 : ℕ
⊢ MeasurableSet.{u_1} (α := α) (⋃ (_ : i_1 < k), 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₁ : 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)
i_1 : ℕ
⊢ MeasurableSet.{u_1} (α := α) (⋃ (_ : i_1 < k), 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₁ : 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
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (l : ℕ) ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) a b

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

Premises used: Iff.mpr, Set.disjoint_iUnion_left