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 ≤[i \ ∅] 0
hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < 0), s.restrictNonposSeq i k] 0
left : s.someExistsOneDivLT (i \ ∅) ⊆ i \ ∅
left_1 : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
h : 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ∅)) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))

Tactic:
lt_trans Nat.one_div_pos_of_nat h

Premises used: lt_trans, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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_1 : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
h : 1 / HAdd.hAdd (α := ℝ) (↑(s.findExistsOneDivLT (i \ ∅)) : ℝ) 1 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ∅))

Tactic:
exact lt_trans Nat.one_div_pos_of_nat h

Premises used: lt_trans, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
succ : 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i (n + 1))

Tactic:
rw [restrictNonposSeq_succ]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_succ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
⊢ i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k ⊆ i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
refine : MeasurableSet (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
⊢ ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k] 0

Tactic:
refine mt (restrict_le_zero_subset _ ?_ (by simp)) hn

Premises used: mt, MeasureTheory.VectorMeasure.restrict_le_zero_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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 + 1), s.restrictNonposSeq i k)

Tactic:
measurable_of_not_restrict_le_zero _ hn

Premises used: MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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 :
  Eq.{u_1 + 1} (α := ℕ → Set α) (fun (k : ℕ) ↦ ⋃ (_ : k ≤ n), s.restrictNonposSeq i k) fun (k : ℕ) ↦
    ⋃ (_ : k < n + 1), s.restrictNonposSeq i k
⊢ MeasurableSet (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)

Tactic:
convert! measurable_of_not_restrict_le_zero _ hn using 3

Premises used: MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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 : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (_ : x ≤ n), s.restrictNonposSeq i x) (⋃ (_ : x ≤ n), s.restrictNonposSeq i x)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (_ : x ≤ n), s.restrictNonposSeq i x) (⋃ (_ : x < n + 1), s.restrictNonposSeq i x)

Tactic:
rw [Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
⊢ Eq.{u_1 + 1} (α := ℕ → Set α) (fun (k : ℕ) ↦ ⋃ (_ : k ≤ n), s.restrictNonposSeq i k) fun (k : ℕ) ↦
    ⋃ (_ : k < n + 1), s.restrictNonposSeq i k

Tactic:
exact funext fun x => by rw [Nat.lt_succ_iff]

Premises used: funext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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

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]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
⊢ 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⟩

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
⊢ MeasurableSet (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))

Tactic:
rcases someExistsOneDivLT_spec h₁ with ⟨_, _, h⟩

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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))
⊢ 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⟩

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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_1 : MeasurableSet (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
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))
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))

Tactic:
lt_trans Nat.one_div_pos_of_nat h

Premises used: lt_trans, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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_1 : MeasurableSet (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))
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))
⊢ 0 < (↑s : Set α → ℝ) (s.someExistsOneDivLT (i \ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), s.restrictNonposSeq i k))

Tactic:
exact lt_trans Nat.one_div_pos_of_nat h

Premises used: lt_trans, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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)
succ :
  ∀ (n : ℕ) (hn : ¬s ≤[i \ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s.restrictNonposSeq i k] 0),
    0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i (n + 1))
⊢ 0 < (↑s : Set α → ℝ) (s.restrictNonposSeq i n)

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

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq, _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_spec, Set.diff_empty, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_succ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
zero : MeasurableSet (s.restrictNonposSeq i 0)
succ : ∀ (n : ℕ), MeasurableSet (s.restrictNonposSeq i (n + 1))
⊢ MeasurableSet (s.restrictNonposSeq i n)

Tactic:
cases n
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
zero : MeasurableSet (s.someExistsOneDivLT (i \ ∅))
⊢ MeasurableSet (s.restrictNonposSeq i 0)

Tactic:
rw [restrictNonposSeq]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.someExistsOneDivLT (i \ ∅))

Tactic:
someExistsOneDivLT_measurableSet

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.someExistsOneDivLT (i \ ∅))

Tactic:
exact someExistsOneDivLT_measurableSet

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
succ :
  MeasurableSet
    (s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k))
⊢ MeasurableSet (s.restrictNonposSeq i (n + 1))

Tactic:
rw [restrictNonposSeq]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ MeasurableSet
    (s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k))

Tactic:
someExistsOneDivLT_measurableSet

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
⊢ MeasurableSet
    (s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n),
            have this := ⋯;
            s.restrictNonposSeq i k))

Tactic:
exact someExistsOneDivLT_measurableSet

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_measurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n < m
rw : ∀ (x : α), x ∉ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
succ : ∀ (n_1 : ℕ) (h : n < n_1 + 1) (hx₂ : x ∈ s.restrictNonposSeq i (n_1 + 1)), False
⊢ False

Tactic:
cases m
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n : ℕ
x : α
hx₁ : x ∈ s.restrictNonposSeq i n
h : n < 0
hx₂ : x ∈ s.restrictNonposSeq i 0
⊢ False

Tactic:
lia
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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)
⊢ x ∈
    s.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n_1),
            have this := ⋯;
            s.restrictNonposSeq i k)

Tactic:
rw [restrictNonposSeq] at hx₂

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n_1),
            have this := ⋯;
            s.restrictNonposSeq i k)
⊢ False

Tactic:
(someExistsOneDivLT_subset hx₂).2
        (Set.mem_iUnion.2 ⟨n, Set.mem_iUnion.2 ⟨Nat.lt_succ_iff.mp h, hx₁⟩⟩)

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset, Iff.mpr, Set.mem_iUnion, And.right, Nat.lt_succ_iff, Exists.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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.someExistsOneDivLT
      (i \
        ⋃ (k : ℕ),
          ⋃ (H : k ≤ n_1),
            have this := ⋯;
            s.restrictNonposSeq i k)
⊢ False

Tactic:
exact
      (someExistsOneDivLT_subset hx₂).2
        (Set.mem_iUnion.2 ⟨n, Set.mem_iUnion.2 ⟨Nat.lt_succ_iff.mp h, hx₁⟩⟩)

Premises used: _private.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset, Iff.mpr, Set.mem_iUnion, And.right, Nat.lt_succ_iff, Exists.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
rw : s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
⊢ (Disjoint on s.restrictNonposSeq i) n m

Tactic:
rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]

Premises used: Function.onFun, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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 = ∅
inr : ∀ (h : m < n), s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
rcases lt_or_gt_of_ne h with (h | h)

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h_1 : n ≠ m
h : n < m
inl inl₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
rw [restrictNonposSeq_disjoint' h]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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 = ∅
inr₁ inr₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ s.restrictNonposSeq i n ∩ s.restrictNonposSeq i m = ∅

Tactic:
rw [Set.inter_comm, restrictNonposSeq_disjoint' h]

Premises used: _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint', Set.inter_comm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
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
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₁ : 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

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₁ : 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

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₁ : MeasurableSet i
hi₂ : (↑s : Set α → ℝ) i < 0
hn : ¬∀ (n : ℕ), ¬s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
h : ¬s ≤[i] 0
⊢ ∃ (n : ℕ), s ≤[i \ ⋃ (l : ℕ), ⋃ (_ : l < n), s.restrictNonposSeq i l] 0

Tactic:
push Not at hn

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

Tactic:
⟨i \ ⋃ l < k, restrictNonposSeq s i l, hi₁.diff hmeas, Set.diff_subset, hk₂, ?_⟩

Premises used: MeasurableSet.diff, Set.diff_subset, _private.0.MeasureTheory.SignedMeasure.restrictNonposSeq, SDiff.sdiff, And.intro, Exists.intro, Set.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)
neg : (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ (↑s : Set α → ℝ) j < 0

Tactic:
refine ⟨i \ ⋃ l < k, restrictNonposSeq s i l, hi₁.diff hmeas, Set.diff_subset, hk₂, ?_⟩
-- 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 : (↑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)
neg₃ : ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l ⊆ i
⊢ (↑s : Set α → ℝ) (i \ ⋃ (l : ℕ), ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0

Tactic:
rw [of_diff hmeas hi₁, s.of_disjoint_iUnion]

Premises used: MeasureTheory.VectorMeasure.of_diff, MeasureTheory.VectorMeasure.of_disjoint_iUnion