awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
⊢ (↑0 : Set α → ℝ) C ≤ (↑s : Set α → ℝ) C
have by_contra! : ∀ (hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C), False
Tactic: by_contra! hC₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
⊢ False
have rcases : ∀ (D : Set α) (hD₁ : MeasurableSet D) (hD : D ⊆ C) (hD₂ : s ≤[D] 0) (hD₃ : (↑s : Set α → ℝ) D < 0), False
Tactic: rcases exists_subset_restrict_nonpos hC₂ with ⟨D, hD₁, hD, hD₂, hD₃⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
⊢ (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
have rw : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D < (↑s : Set α → ℝ) A
Tactic: rw [← hA₃,
      of_union (Set.disjoint_of_subset_right (Set.Subset.trans hD hC₁) disjoint_compl_right) hA₁
        hD₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
⊢ (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D < (↑s : Set α → ℝ) A
have linarith : (↑s : Set α → ℝ) A ≤ (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D →
  (↑s : Set α → ℝ) D - 0 + ((↑s : Set α → ℝ) A - ((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) D)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
⊢ False
have this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
Tactic: have : s (A ∪ D) < sInf s.measureOfNegatives := by
    rw [← hA₃,
      of_union (Set.disjoint_of_subset_right (Set.Subset.trans hD hC₁) disjoint_compl_right) hA₁
        hD₁]
    linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ False
have refine : sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) (A ∪ D)
Tactic: refine not_le.2 this ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
⊢ sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) (A ∪ D)
have refine_1 : MeasurableSet (A ∪ D)
Tactic: refine csInf_le bddBelow_measureOfNegatives ⟨A ∪ D, ⟨?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : (n : ℕ) → Set α
hB :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set α)) {B : Set α | MeasurableSet B ∧ s ≤[B] 0} (B n) ∧ (↑s : Set α → ℝ) (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
hB₂ : ∀ (n : ℕ), s ≤[B n] 0
A : Set α := ⋃ (n : ℕ), B n
hA : A = ⋃ (n : ℕ), B n
hA₁ : MeasurableSet A
hA₂ : s ≤[A] 0
hA₃ : (↑s : Set α → ℝ) A = sInf s.measureOfNegatives
C : Set α
h : MeasurableSet C
hC₁ : C ⊆ Aᶜ
hC₂ : (↑s : Set α → ℝ) C < (↑0 : Set α → ℝ) C
D : Set α
hD₁ : MeasurableSet D
hD : D ⊆ C
hD₂ : s ≤[D] 0
hD₃ : (↑s : Set α → ℝ) D < 0
this : (↑s : Set α → ℝ) (A ∪ D) < sInf s.measureOfNegatives
refine_1 : MeasurableSet (A ∪ D)
⊢ sInf s.measureOfNegatives ≤ (↑s : Set α → ℝ) (A ∪ D)
have refine_2 : s ≤[A ∪ D] 0
Tactic: refine csInf_le bddBelow_measureOfNegatives ⟨A ∪ D, ⟨?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have rw : ∀
  (hi' :
    (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
      ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
  (hj' :
    (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
      ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
  (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
Tactic: rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
Cleared hypotheses: hi', hj'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
rw :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' :
      (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
        ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have rw₁ : ∀
  (hi' :
    (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
      ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
  (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
  MeasurableSet j
Tactic: rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
Cleared hypotheses: hi', hj'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
rw :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' :
      (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
        ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
rw₁ :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet j
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have rw₂ : ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
  (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
  MeasurableSet i
Tactic: rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
Cleared hypotheses: hi', hj'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
rw :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' :
      (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
        ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
rw₁ :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet j
rw₂ :
  ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet i
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have rw₃ : ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
  (hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0), MeasurableSet jᶜ
Tactic: rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
Cleared hypotheses: hi', hj'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
rw :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' :
      (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
        ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
rw₁ :
  ∀
    (hi' :
      (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
        ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet j
rw₂ :
  ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1),
    MeasurableSet i
rw₃ :
  ∀ (hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j)
    (hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0), MeasurableSet jᶜ
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have rw₄ : MeasurableSet iᶜ
Tactic: rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have left : (↑s : Set α → ℝ) (i ∆ j) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
left : (↑s : Set α → ℝ) (i ∆ j) = 0
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0 ∧ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have right : (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0
have left : Disjoint (jᶜ ∩ i) (iᶜ ∩ j)
Tactic: rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, of_union,
      le_antisymm (hi'.2 (hi.compl.inter hj) Set.inter_subset_left)
        (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
      le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left)
        (hi'.1 (hj.compl.inter hi) Set.inter_subset_right),
      zero_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
left : Disjoint (jᶜ ∩ i) (iᶜ ∩ j)
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0
have left₁ : MeasurableSet (jᶜ ∩ i)
Tactic: rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, of_union,
      le_antisymm (hi'.2 (hi.compl.inter hj) Set.inter_subset_left)
        (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
      le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left)
        (hi'.1 (hj.compl.inter hi) Set.inter_subset_right),
      zero_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
left : Disjoint (jᶜ ∩ i) (iᶜ ∩ j)
left₁ : MeasurableSet (jᶜ ∩ i)
⊢ (↑s : Set α → ℝ) (i ∆ j) = 0
have left₂ : MeasurableSet (iᶜ ∩ j)
Tactic: rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, of_union,
      le_antisymm (hi'.2 (hi.compl.inter hj) Set.inter_subset_left)
        (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
      le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left)
        (hi'.1 (hj.compl.inter hi) Set.inter_subset_right),
      zero_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have right : Disjoint (j ∩ iᶜ) (i ∩ jᶜ)
Tactic: rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, compl_compl,
      compl_compl, of_union,
      le_antisymm (hi'.2 (hj.inter hi.compl) Set.inter_subset_right)
        (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
      le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right)
        (hi'.1 (hi.inter hj.compl) Set.inter_subset_left),
      zero_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
right : Disjoint (j ∩ iᶜ) (i ∩ jᶜ)
⊢ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have right₁ : MeasurableSet (j ∩ iᶜ)
Tactic: rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, compl_compl,
      compl_compl, of_union,
      le_antisymm (hi'.2 (hj.inter hi.compl) Set.inter_subset_right)
        (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
      le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right)
        (hi'.1 (hi.inter hj.compl) Set.inter_subset_left),
      zero_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
right : Disjoint (j ∩ iᶜ) (i ∩ jᶜ)
right₁ : MeasurableSet (j ∩ iᶜ)
⊢ (↑s : Set α → ℝ) (iᶜ ∆ jᶜ) = 0
have right₂ : MeasurableSet (i ∩ jᶜ)
Tactic: rw [Set.symmDiff_def, Set.diff_eq_compl_inter, Set.diff_eq_compl_inter, compl_compl,
      compl_compl, of_union,
      le_antisymm (hi'.2 (hj.inter hi.compl) Set.inter_subset_right)
        (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
      le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right)
        (hi'.1 (hi.inter hj.compl) Set.inter_subset_left),
      zero_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (↑r : ℝ) • j = r • j
have rw : (if 0 ≤ (↑r : ℝ) then (↑r : ℝ).toNNReal • j else -((-(↑r : ℝ)).toNNReal • j)) = r • j
Tactic: rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
rw : (if 0 ≤ (↑r : ℝ) then (↑r : ℝ).toNNReal • j else -((-(↑r : ℝ)).toNNReal • j)) = r • j
⊢ (↑r : ℝ) • j = r • j
have rw₁ : (↑r : ℝ).toNNReal • j = r • j
Tactic: rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
rw : (if 0 ≤ (↑r : ℝ) then (↑r : ℝ).toNNReal • j else -((-(↑r : ℝ)).toNNReal • j)) = r • j
rw₁ : (↑r : ℝ).toNNReal • j = r • j
⊢ (↑r : ℝ) • j = r • j
have rw₂ : r • j = r • j
Tactic: rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r • j).posPart = r.toNNReal • j.posPart
have rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = r.toNNReal • j.posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_pos hr]