awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ (↑μ : Set α → ℝ≥0∞) t = 0
have mpr : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← VectorMeasure.ennrealToMeasure_apply hmt]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ Eq (α := ℝ≥0∞) ((μ - ν : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : μ.restrict s - ν.restrict s = 0
Tactic: rw [← restrict_eq_zero, restrict_sub_eq_restrict_sub_restrict hs.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ - ν ⟂ₘ ν - μ
have obtain : ∀ (s : Set X) (hs : IsHahnDecomposition μ ν s), μ - ν ⟂ₘ ν - μ
Tactic: obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
⊢ ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
have hmeas : MeasurableSet s
Tactic: have hmeas := hs.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
⊢ ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
have rw : ((ν - μ).restrict s + μ.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s
Tactic: rw [eq_sub_iff_add_eq, toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas,
    ← toSignedMeasure_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
⊢ ((ν - μ).restrict s + μ.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s
have simp : (ν.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s
Tactic: simp only [restrict_sub_eq_restrict_sub_restrict, hmeas, sub_add_cancel_of_le hs.le_on]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have obtain : ∀ (s : Set X) (hs : IsHahnDecomposition μ ν s),
  μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
Tactic: obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have hsc : IsHahnDecomposition ν μ sᶜ
Tactic: have hsc := hs.compl
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have h₁ : ((ν - μ).restrict s).toSignedMeasure =
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
Tactic: have h₁ := toSignedMeasure_restrict_sub hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have h₂ : ((μ - ν).restrict sᶜ).toSignedMeasure =
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
Tactic: have h₂ := toSignedMeasure_restrict_sub hsc
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
Tactic: have h₁' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
    sub_apply_eq_zero_of_isHahnDecomposition hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
Tactic: have h₂' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
  sub_apply_eq_zero_of_isHahnDecomposition hsc
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₁ : VectorMeasure.restrict (μ - ν).toSignedMeasure s + VectorMeasure.restrict (μ - ν).toSignedMeasure sᶜ =
  (μ - ν).toSignedMeasure
Tactic: have partition₁ := VectorMeasure.restrict_add_restrict_compl (μ - ν).toSignedMeasure
    hs.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict (μ - ν).toSignedMeasure s + VectorMeasure.restrict (μ - ν).toSignedMeasure sᶜ =
    (μ - ν).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₂ : VectorMeasure.restrict (ν - μ).toSignedMeasure s + VectorMeasure.restrict (ν - μ).toSignedMeasure sᶜ =
  (ν - μ).toSignedMeasure
Tactic: have partition₂ := VectorMeasure.restrict_add_restrict_compl (ν - μ).toSignedMeasure
    hs.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict (μ - ν).toSignedMeasure s + VectorMeasure.restrict (μ - ν).toSignedMeasure sᶜ =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict (ν - μ).toSignedMeasure s + VectorMeasure.restrict (ν - μ).toSignedMeasure sᶜ =
    (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₃ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
Tactic: rw [toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet,
    toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl]
    at partition₁ partition₂
Cleared hypotheses: partition₁, partition₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict (μ - ν).toSignedMeasure s + VectorMeasure.restrict (μ - ν).toSignedMeasure sᶜ =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict (ν - μ).toSignedMeasure s + VectorMeasure.restrict (ν - μ).toSignedMeasure sᶜ =
    (ν - μ).toSignedMeasure
partition₃ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₄ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
Tactic: rw [toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet,
    toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl]
    at partition₁ partition₂
Cleared hypotheses: partition₁, partition₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₃ : toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
  (μ - ν).toSignedMeasure
Tactic: rw [h₁', h₂] at partition₁
Cleared hypotheses: partition₁, partition₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₃ : VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
  (ν - μ).toSignedMeasure
Tactic: rw [h₁, h₂'] at partition₂
Cleared hypotheses: partition₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
    (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₃ : VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
Tactic: simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂
Cleared hypotheses: partition₁, partition₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
    (ν - μ).toSignedMeasure
partition₃ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have partition₄ : VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure
Tactic: simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂
Cleared hypotheses: partition₁, partition₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
have rw : VectorMeasure.restrict μ.toSignedMeasure s + VectorMeasure.restrict μ.toSignedMeasure sᶜ -
    (VectorMeasure.restrict ν.toSignedMeasure s + VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ -
    (VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0)
Tactic: rw [← VectorMeasure.restrict_add_restrict_compl μ.toSignedMeasure hs.measurableSet,
    ← VectorMeasure.restrict_add_restrict_compl ν.toSignedMeasure hs.measurableSet,
    ← partition₁, ← partition₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
have simp_rw : (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart.toSignedMeasure -
    (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
  μ.toSignedMeasure - ν.toSignedMeasure
Tactic: simp_rw [JordanDecomposition.toSignedMeasure, jordanDecompositionOfToSignedMeasureSub_posPart,
    jordanDecompositionOfToSignedMeasureSub_negPart, ← sub_toSignedMeasure_eq_toSignedMeasure_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
simp_rw :
  (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart.toSignedMeasure -
      (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
    μ.toSignedMeasure - ν.toSignedMeasure
⊢ (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
have simp_rw₁ : (μ - ν).toSignedMeasure - (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
  μ.toSignedMeasure - ν.toSignedMeasure
Tactic: simp_rw [JordanDecomposition.toSignedMeasure, jordanDecompositionOfToSignedMeasureSub_posPart,
    jordanDecompositionOfToSignedMeasureSub_negPart, ← sub_toSignedMeasure_eq_toSignedMeasure_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
simp_rw :
  (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart.toSignedMeasure -
      (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
    μ.toSignedMeasure - ν.toSignedMeasure
simp_rw₁ :
  (μ - ν).toSignedMeasure - (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
    μ.toSignedMeasure - ν.toSignedMeasure
⊢ (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
have simp_rw₂ : (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
Tactic: simp_rw [JordanDecomposition.toSignedMeasure, jordanDecompositionOfToSignedMeasureSub_posPart,
    jordanDecompositionOfToSignedMeasureSub_negPart, ← sub_toSignedMeasure_eq_toSignedMeasure_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν
have a : (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.toSignedMeasure =
  (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
Tactic: apply JordanDecomposition.toSignedMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.toSignedMeasure =
    (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
have a : μ.toSignedMeasure - ν.toSignedMeasure = (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
Tactic: rw [SignedMeasure.toSignedMeasure_toJordanDecomposition,
    jordanDecompositionOfToSignedMeasureSub_toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
a : μ.toSignedMeasure - ν.toSignedMeasure = (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
⊢ (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.toSignedMeasure =
    (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
have a₁ : μ.toSignedMeasure - ν.toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
Tactic: rw [SignedMeasure.toSignedMeasure_toJordanDecomposition,
    jordanDecompositionOfToSignedMeasureSub_toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
⊢ (-s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
have rw : s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
Tactic: rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
⊢ (-s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
have rw : s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
Tactic: rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]