awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
left : s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
have left₁ : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
Tactic: rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
left : s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅
left₁ : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
have h : 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ∅)) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
Tactic: rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i (n + 1))
have succ : 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
Tactic: rw [restrictNonposSeq_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
have refine : MeasurableSet (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
Tactic: refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ MeasurableSet (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
have h : Eq.{u_1 + 1} (α := ℕ → Set α) (fun (k : ℕ) ↦ ⋃ (_ : k ≤ n), s.restrictNonposSeq i k) fun (k : ℕ) ↦
  ⋃ (_ : k < n + 1), s.restrictNonposSeq i k
Tactic: convert! measurable_of_not_restrict_le_zero _ hn using 3
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
x : ℕ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (_ : x ≤ n), s.restrictNonposSeq i x) (⋃ (_ : x < n + 1), s.restrictNonposSeq i x)
have rw : Eq.{u_1 + 1} (α := Set α) (⋃ (_ : x ≤ n), s.restrictNonposSeq i x) (⋃ (_ : x ≤ n), s.restrictNonposSeq i x)
Tactic: rw [Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
have h₁ : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
Tactic: have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
      refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn
      convert! measurable_of_not_restrict_le_zero _ hn using 3
      exact funext fun x => by rw [Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
h₁ : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
have left : s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k) ⊆
  i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k
Tactic: rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
h₁ : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
left :
  s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k) ⊆
    i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
have left₁ : MeasurableSet (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
Tactic: rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0
h₁ : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0
left :
  s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k) ⊆
    i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k
left₁ : MeasurableSet (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
have h : 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)) : ℝ) 1 <
  (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
Tactic: rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n), s.restrictNonposSeq i k] 0
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i n)
have zero : ∀ (hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0), 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i 0)
Tactic: cases n with
  | zero =>
    rw [restrictNonposSeq]; rw [← @Set.diff_empty _ i] at hi₂
    rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h
  | succ n =>
    rw [restrictNonposSeq_succ]
    have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
      refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn
      convert! measurable_of_not_restrict_le_zero _ hn using 3
      exact funext fun x => by rw [Nat.lt_succ_iff]
    rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₂ : ¬s ≤[i] 0
n : ℕ
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n), s.restrictNonposSeq i k] 0
zero :
  ∀ (hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0), 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i 0)
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i n)
have succ : ∀ (n : ℕ) (hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0),
  0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i (n + 1))
Tactic: cases n with
  | zero =>
    rw [restrictNonposSeq]; rw [← @Set.diff_empty _ i] at hi₂
    rcases someExistsOneDivLT_spec hi₂ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h
  | succ n =>
    rw [restrictNonposSeq_succ]
    have h₁ : ¬s ≤[i \ ⋃ (k : ℕ) (_ : k ≤ n), restrictNonposSeq s i k] 0 := by
      refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn
      convert! measurable_of_not_restrict_le_zero _ hn using 3
      exact funext fun x => by rw [Nat.lt_succ_iff]
    rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩
    exact lt_trans Nat.one_div_pos_of_nat h
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i n)
have zero : MeasurableSet (s.restrictNonposSeq i 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
zero : MeasurableSet (s.restrictNonposSeq i 0)
⊢ MeasurableSet (s.restrictNonposSeq i n)
have succ : ∀ (n : ℕ), MeasurableSet (s.restrictNonposSeq i (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.restrictNonposSeq i 0)
have zero : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
Tactic: rw [restrictNonposSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i (n + 1))
have succ : MeasurableSet
  (s.someExistsOneDivLT
    (i \
      ⋃ (k : ℕ),
        ⋃ (H : k ≤ n),
          have this := sorry;
          s.restrictNonposSeq i k))
Tactic: rw [restrictNonposSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
have rw : ∀ (x : α), x ∉ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
hx₂ : x ∈ s.restrictNonposSeq i m
⊢ False
have zero : ∀ (h : n < 0) (hx₂ : x ∈ s.restrictNonposSeq i 0), False
Tactic: cases m
Cleared hypotheses: m, h, hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
hx₂ : x ∈ s.restrictNonposSeq i m
zero : ∀ (h : n < 0) (hx₂ : x ∈ s.restrictNonposSeq i 0), False
⊢ False
have succ : ∀ (n_1 : ℕ) (h : n < n_1 + 1) (hx₂ : x ∈ s.restrictNonposSeq i (n_1 + 1)), False
Tactic: cases m
Cleared hypotheses: m, h, hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
n_1 : ℕ
h : n < n_1 + 1
hx₂ : x ∈ s.restrictNonposSeq i (n_1 + 1)
⊢ False
have hx₃ : x ∈
  s.someExistsOneDivLT
    (i \
      ⋃ (k : ℕ),
        ⋃ (H : k ≤ n_1),
          have this := sorry;
          s.restrictNonposSeq i k)
Tactic: rw [restrictNonposSeq] at hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ (Disjoint on s.restrictNonposSeq i) n m
have rw : s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
Tactic: rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
have inl : ∀ (h : n < m), s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
Tactic: rcases lt_or_gt_of_ne h with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
inl : ∀ (h : n < m), s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
have inr : ∀ (h : m < n), s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
Tactic: rcases lt_or_gt_of_ne h with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h_1 : n ≠ m
h : n < m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
have inl : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [restrictNonposSeq_disjoint' h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h_1 : n ≠ m
h : m < n
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
have inr : s.restrictNonposSeq i m ∩ s.restrictNonposSeq i n = ∅
Tactic: rw [Set.inter_comm, restrictNonposSeq_disjoint' h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h_1 : n ≠ m
h : m < n
inr : s.restrictNonposSeq i m ∩ s.restrictNonposSeq i n = ∅
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
have inr₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Set.inter_comm, restrictNonposSeq_disjoint' h]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) 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
have pos : ∀ (h : s ≤[i] 0), ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
Tactic: by_cases h : s ≤[i] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
pos : ∀ (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
have neg : ∀ (h : ¬s ≤[i] 0), ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
Tactic: by_cases h : s ≤[i] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
h : ¬s ≤[i] 0
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
have hn₁ : ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
Tactic: push Not at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
have hk₂ : s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
Tactic: have hk₂ : s ≤[i \ ⋃ l < k, restrictNonposSeq s i l] 0 := Nat.find_spec hn
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
have hmeas : MeasurableSet.{u_1} (α := α) (⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l)
Tactic: have hmeas : MeasurableSet (⋃ (l : ℕ) (_ : l < k), restrictNonposSeq s i l) :=
    MeasurableSet.iUnion fun _ => MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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)
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0
have neg : (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0
Tactic: refine ⟨i \ ⋃ l < k, restrictNonposSeq s i l, hi₁.diff hmeas, Set.diff_subset, hk₂, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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)
⊢ (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0
have neg : (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0
Tactic: rw [of_diff hmeas hi₁, s.of_disjoint_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0
⊢ (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0
have neg₁ : ∀ (i_1 : ℕ), MeasurableSet.{u_1} (α := α) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)
Tactic: rw [of_diff hmeas hi₁, s.of_disjoint_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0
neg₁ : ∀ (i_1 : ℕ), MeasurableSet.{u_1} (α := α) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)
⊢ (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0
have neg₂ : Pairwise (α := ℕ)
  (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (l : ℕ) ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l)
Tactic: rw [of_diff hmeas hi₁, s.of_disjoint_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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 : (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0
neg₁ : ∀ (i_1 : ℕ), MeasurableSet.{u_1} (α := α) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)
neg₂ :
  Pairwise (α := ℕ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (l : ℕ) ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0
have neg₃ : ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l ⊆ i
Tactic: rw [of_diff hmeas hi₁, s.of_disjoint_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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)
have refine : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k] 0
Tactic: refine le_of_lt (measure_of_restrictNonposSeq h _ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
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
have refine : MeasurableSet.{u_1} (α := α) (⋃ (k : ℕ), ⋃ (_ : k < l), s.restrictNonposSeq i k)
Tactic: refine mt (restrict_le_zero_subset _ (hi₁.diff ?_) (Set.Subset.refl _)) (Nat.find_min hn hl)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
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)
⊢ (↑s : Set α → ℝ) i - ∑' (i_1 : ℕ), (↑s : Set α → ℝ) (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0
have h₁ : ∀ 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 _